diff --git a/creusot/src/backend.rs b/creusot/src/backend.rs index 4c529d7a6..11435a5ba 100644 --- a/creusot/src/backend.rs +++ b/creusot/src/backend.rs @@ -5,6 +5,7 @@ use rustc_span::{RealFileName, Span}; use crate::{ contracts_items::{is_resolve_function, is_spec, is_trusted}, ctx::{ItemType, TranslatedItem, TranslationCtx}, + error::CannotFetchThir, naming::ModulePath, options::SpanMode, run_why3::SpanMap, @@ -52,7 +53,7 @@ impl<'tcx> Why3Generator<'tcx> { Why3Generator { ctx, functions: Default::default(), span_map: Default::default() } } - pub(crate) fn translate(&mut self, def_id: DefId) { + pub(crate) fn translate(&mut self, def_id: DefId) -> Result<(), CannotFetchThir> { debug!("translating {:?}", def_id); // eprintln!("{:?}", self.param_env(def_id)); @@ -66,7 +67,7 @@ impl<'tcx> Why3Generator<'tcx> { self.functions.push(TranslatedItem::Logic { proof_modl: None }); } ItemType::Logic { .. } | ItemType::Predicate { .. } => { - let proof_modl = logic::translate_logic_or_predicate(self, def_id); + let proof_modl = logic::translate_logic_or_predicate(self, def_id)?; self.functions.push(TranslatedItem::Logic { proof_modl }); } ItemType::Program => { @@ -80,9 +81,10 @@ impl<'tcx> Why3Generator<'tcx> { ), _ => (), } + Ok(()) } - pub(crate) fn modules<'a>(&'a mut self) -> impl Iterator + 'a { + pub(crate) fn modules(&mut self) -> impl Iterator + '_ { self.functions.drain(..) } @@ -148,11 +150,8 @@ impl<'tcx> Why3Generator<'tcx> { None => return None, // The last segment is CrateRoot. Skip it. Some(parent_id) => parent_id, }; - match key.disambiguated_data.data { - rustc_hir::definitions::DefPathData::Impl => { - return Some(display_impl_subject(&tcx.impl_subject(id).skip_binder())) - } - _ => {} + if key.disambiguated_data.data == rustc_hir::definitions::DefPathData::Impl { + return Some(display_impl_subject(&tcx.impl_subject(id).skip_binder())); } id.index = parent_id; } diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs index 7ec6a41bc..5497db6f7 100644 --- a/creusot/src/backend/clone_map/elaborator.rs +++ b/creusot/src/backend/clone_map/elaborator.rs @@ -130,7 +130,7 @@ impl DepElab for ProgElab { }; let coma = program::to_why(ctx, &mut names, name, bid); - return vec![Decl::Coma(coma)]; + vec![Decl::Coma(coma)] } } @@ -289,23 +289,18 @@ impl<'a, 'tcx> Expander<'a, 'tcx> { param_env: ParamEnv<'tcx>, initial: impl Iterator>, ) -> Self { - let exp = Self { + Self { graph: Default::default(), namer, self_key, param_env, expansion_queue: initial.map(|b| (self_key, Strength::Strong, b)).collect(), dep_bodies: Default::default(), - }; - exp + } } fn namer(&mut self, source: Dependency<'tcx>) -> ExpansionProxy<'_, 'tcx> { - ExpansionProxy { - namer: &mut self.namer, - expansion_queue: &mut self.expansion_queue, - source, - } + ExpansionProxy { namer: self.namer, expansion_queue: &mut self.expansion_queue, source } } /// Expand the graph with new entries @@ -421,11 +416,7 @@ fn expand_laws<'tcx>( } } -fn val<'tcx>( - ctx: &mut Why3Generator<'tcx>, - mut sig: Signature, - kind: Option, -) -> Vec { +fn val(ctx: &mut Why3Generator, mut sig: Signature, kind: Option) -> Vec { sig.contract.variant = Vec::new(); if let Some(k) = kind { let ax = if !sig.contract.is_empty() { Some(spec_axiom(&sig)) } else { None }; @@ -473,7 +464,7 @@ fn resolve_term<'tcx>( } traits::TraitResolved::UnknownFound | traits::TraitResolved::UnknownNotFound => { // We don't know the instance => body is opaque - return None; + None } traits::TraitResolved::NoInstance => { // We know there is no instance => body is true @@ -603,7 +594,7 @@ fn term<'tcx>( let ty = ctx.type_of(def_id).instantiate(ctx.tcx, subst); let ty = ctx.tcx.normalize_erasing_regions(param_env, ty); let span = ctx.def_span(def_id); - let res = from_ty_const(&mut ctx.ctx, constant, ty, param_env, span); + let res = from_ty_const(&ctx.ctx, constant, ty, param_env, span); Some(res) } else if is_resolve_function(ctx.tcx, def_id) { resolve_term(ctx, param_env, def_id, subst) @@ -623,7 +614,7 @@ fn term<'tcx>( let TyKind::Closure(did, _) = subst.type_at(1).kind() else { return None }; Some(ctx.closure_contract(*did).unnest.clone().unwrap()) } else { - let term = ctx.term(def_id).unwrap().clone(); + let term = ctx.term_fail_fast(def_id).unwrap().clone(); let term = normalize( ctx.tcx, param_env, diff --git a/creusot/src/backend/logic.rs b/creusot/src/backend/logic.rs index 9b6516d82..7ef8701ec 100644 --- a/creusot/src/backend/logic.rs +++ b/creusot/src/backend/logic.rs @@ -12,12 +12,11 @@ mod vcgen; use self::vcgen::vc; -use super::{is_trusted_function, signature::signature_of, term::lower_pure, Why3Generator}; +use super::{ + is_trusted_function, signature::signature_of, term::lower_pure, CannotFetchThir, Why3Generator, +}; -pub(crate) fn binders_to_args( - ctx: &mut Why3Generator, - binders: Vec, -) -> (Vec, Vec) { +pub(crate) fn binders_to_args(binders: Vec) -> (Vec, Vec) { let mut args = Vec::new(); let mut out_binders = Vec::new(); let mut fresh = 0; @@ -30,11 +29,11 @@ pub(crate) fn binders_to_args( } Binder::UnNamed(_) => unreachable!("unnamed parameter in logical function signature"), Binder::Named(ref nm) => { - args.push(nm.clone().into()); + args.push(nm.clone()); out_binders.push(b); } Binder::Typed(ghost, binders, ty) => { - let (inner_args, inner_binders) = binders_to_args(ctx, binders); + let (inner_args, inner_binders) = binders_to_args(binders); args.extend(inner_args); out_binders.push(Binder::Typed(ghost, inner_binders, ty)); } @@ -43,16 +42,16 @@ pub(crate) fn binders_to_args( (args, out_binders) } -pub(crate) fn translate_logic_or_predicate<'tcx>( - ctx: &mut Why3Generator<'tcx>, +pub(crate) fn translate_logic_or_predicate( + ctx: &mut Why3Generator, def_id: DefId, -) -> Option { +) -> Result, CannotFetchThir> { let mut names = Dependencies::new(ctx, def_id); // Check that we don't have both `builtins` and a contract at the same time (which are contradictory) if get_builtin(ctx.tcx, def_id).is_some() { if signature_of(ctx, &mut names, "".into(), def_id).contract.is_empty() { - return None; + return Ok(None); } ctx.crash_and_error( @@ -69,14 +68,14 @@ pub(crate) fn translate_logic_or_predicate<'tcx>( || is_trusted_function(ctx.tcx, def_id) || !ctx.has_body(def_id) { - return None; + return Ok(None); } - let term = ctx.ctx.term(def_id).unwrap().clone(); + let term = ctx.ctx.term(def_id)?.unwrap().clone(); let mut body_decls = Vec::new(); - let (arg_names, new_binders) = binders_to_args(ctx, sig.args); + let (arg_names, new_binders) = binders_to_args(sig.args); let param_decls = arg_names.iter().zip(new_binders.iter()).map(|(nm, binder)| { Decl::LogicDecl(LogicDecl { @@ -129,7 +128,7 @@ pub(crate) fn translate_logic_or_predicate<'tcx>( let meta = ctx.display_impl_of(def_id); let path = ctx.module_path(def_id); let name = path.why3_ident(); - Some(FileModule { path, modl: Module { name, decls, attrs, meta } }) + Ok(Some(FileModule { path, modl: Module { name, decls, attrs, meta } })) } pub(crate) fn lower_logical_defn<'tcx, N: Namer<'tcx>>( @@ -234,8 +233,8 @@ fn limited_function_encode( let lim_call = function_call(&lim_sig); lim_sig.trigger = Some(Trigger::single(lim_call.clone())); decls.push(Decl::LogicDecl(LogicDecl { kind, sig: lim_sig })); - decls.push(Decl::Axiom(definition_axiom(&sig, body, "def"))); - decls.push(Decl::Axiom(definition_axiom(&sig, lim_call, "def_lim"))); + decls.push(Decl::Axiom(definition_axiom(sig, body, "def"))); + decls.push(Decl::Axiom(definition_axiom(sig, lim_call, "def_lim"))); } pub(crate) fn spec_axiom(sig: &Signature) -> Axiom { diff --git a/creusot/src/backend/logic/vcgen.rs b/creusot/src/backend/logic/vcgen.rs index b87c2ad0b..83806a9fc 100644 --- a/creusot/src/backend/logic/vcgen.rs +++ b/creusot/src/backend/logic/vcgen.rs @@ -144,20 +144,20 @@ fn is_structurally_recursive(ctx: &mut Why3Generator<'_>, self_id: DefId, t: &Te let mut binds = Default::default(); pattern.binds(&mut binds); let old_smaller = self.smaller_than.clone(); - self.smaller_than.retain(|nm, _| !binds.contains(&nm)); + self.smaller_than.retain(|nm, _| !binds.contains(nm)); binds.into_iter().for_each(|b| self.smaller_than(b, arg)); self.visit_term(body); self.smaller_than = old_smaller; } TermKind::Match { arms, scrutinee } => { - self.visit_term(&scrutinee); + self.visit_term(scrutinee); for (pat, exp) in arms { let mut binds = Default::default(); pat.binds(&mut binds); let old_smaller = self.smaller_than.clone(); - self.smaller_than.retain(|nm, _| !binds.contains(&nm)); + self.smaller_than.retain(|nm, _| !binds.contains(nm)); binds.into_iter().for_each(|b| self.smaller_than(b, scrutinee)); self.visit_term(exp); self.smaller_than = old_smaller; @@ -176,7 +176,7 @@ fn is_structurally_recursive(ctx: &mut Why3Generator<'_>, self_id: DefId, t: &Te orig_args, }; - s.visit_term(&t); + s.visit_term(t); s.valid() } @@ -299,10 +299,10 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> { // BinOp::Or => self.build_vc(lhs, &|lhs| { // Ok(Exp::if_(lhs, k(Exp::mk_true())?, self.build_vc(rhs, k)?,)) // }), - BinOp::Div => self.build_vc(&lhs, &|lhs| { + BinOp::Div => self.build_vc(lhs, &|lhs| { self.build_vc(rhs, &|rhs| k(Exp::var("div").app(vec![lhs.clone(), rhs]))) }), - _ => self.build_vc(&lhs, &|lhs| { + _ => self.build_vc(lhs, &|lhs| { self.build_vc(rhs, &|rhs| { k(Exp::BinaryOp(binop_to_binop(*op), Box::new(lhs.clone()), Box::new(rhs))) }) @@ -359,9 +359,9 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> { }) } // VC( * T, Q) = VC(T, |t| Q(*t)) - TermKind::Cur { term } => self.build_vc(&term, &|term| k(term.field("current"))), + TermKind::Cur { term } => self.build_vc(term, &|term| k(term.field("current"))), // VC( ^ T, Q) = VC(T, |t| Q(^t)) - TermKind::Fin { term } => self.build_vc(&term, &|term| k(term.field("final"))), + TermKind::Fin { term } => self.build_vc(term, &|term| k(term.field("final"))), // VC(A -> B, Q) = VC(A, VC(B, Q(A -> B))) TermKind::Impl { lhs, rhs } => self.build_vc(lhs, &|lhs| { Ok(Exp::if_(lhs, self.build_vc(rhs, k)?, k(Exp::mk_true())?)) @@ -372,7 +372,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> { && arms.len() == 2 && arms.iter().all(|a| a.0.get_bool().is_some()) => { - self.build_vc(&scrutinee, &|scrut| { + self.build_vc(scrutinee, &|scrut| { let mut arms: Vec<_> = arms .iter() .map(&|arm: &(Pattern<'tcx>, Term<'tcx>)| { @@ -461,11 +461,11 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> { match pat { Pattern::Constructor { variant, fields, substs } => { let fields = - fields.into_iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect(); + fields.iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect(); let substs = self.ctx.borrow().normalize_erasing_regions(self.param_env, *substs); if self.ctx.borrow().def_kind(variant) == DefKind::Variant { Pat::ConsP(self.names.borrow_mut().constructor(*variant, substs), fields) - } else if fields.len() == 0 { + } else if fields.is_empty() { Pat::TupleP(vec![]) } else { Pat::RecP( @@ -500,9 +500,9 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> { Pat::mk_false() } } - Pattern::Tuple(pats) => Pat::TupleP( - pats.into_iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect(), - ), + Pattern::Tuple(pats) => { + Pat::TupleP(pats.iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect()) + } Pattern::Deref { pointee, kind } => match kind { PointerKind::Box | PointerKind::Shr => self.build_pattern_inner(bounds, pointee), PointerKind::Mut => { @@ -516,7 +516,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> { let occ = self.subst.borrow().occ(id); if occ == 0 { - return id.clone(); + id.clone() } else { Ident::from_string(format!("{}_{occ}", &**id)) } @@ -574,7 +574,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> { let top_level_args = self.top_level_args(); let mut subst: Environment = - top_level_args.into_iter().zip(call_args.into_iter().cloned()).collect(); + top_level_args.into_iter().zip(call_args.iter().cloned()).collect(); let orig_variant = self.self_sig().contract.variant.remove(0); let mut rec_var_exp = orig_variant.clone(); rec_var_exp.subst(&mut subst); @@ -588,7 +588,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> { /// Produces the top-level call expression for the function being verified fn top_level_args(&self) -> Vec { let sig = self.self_sig(); - let (arg_names, _) = binders_to_args(*self.ctx.borrow_mut(), sig.args); + let (arg_names, _) = binders_to_args(sig.args); arg_names } @@ -613,7 +613,7 @@ pub(crate) fn get_func_name<'tcx>( // Add dependency names.value(id, subst); - QName::from_string(&a.as_str()).without_search_path() + QName::from_string(a.as_str()).without_search_path() }) .unwrap_or_else(|| names.value(id, subst)) } diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs index 1f0199bf4..83e56d577 100644 --- a/creusot/src/ctx.rs +++ b/creusot/src/ctx.rs @@ -6,7 +6,7 @@ use crate::{ opacity_witness_name, }, creusot_items::{self, CreusotItems}, - error::CreusotResult, + error::{CannotFetchThir, CreusotResult, Error}, metadata::{BinaryMetadata, Metadata}, options::Options, specification::{pre_sig_of, PreSignature}, @@ -36,6 +36,7 @@ use rustc_infer::traits::ObligationCause; use rustc_macros::{TypeFoldable, TypeVisitable}; use rustc_middle::{ mir::{Body, Promoted, TerminatorKind}, + thir, ty::{ Clause, GenericArg, GenericArgsRef, ParamEnv, Predicate, ResolverAstLowering, Ty, TyCtxt, Visibility, @@ -115,7 +116,7 @@ pub enum ItemType { } impl ItemType { - pub(crate) fn to_str(&self) -> &str { + pub(crate) fn to_str(self) -> &'static str { match self { ItemType::Logic { prophetic: false } => "logic function", ItemType::Logic { prophetic: true } => "prophetic logic function", @@ -194,12 +195,12 @@ fn gather_params_open_inv(tcx: TyCtxt) -> HashMap> { let (resolver, cr) = &*tcx.resolver_for_lowering().borrow(); - let mut visit = VisitFns(HashMap::new(), &resolver); - visit.visit_crate(&*cr); + let mut visit = VisitFns(HashMap::new(), resolver); + visit.visit_crate(cr); visit.0 } -impl<'tcx, 'sess> TranslationCtx<'tcx> { +impl<'tcx> TranslationCtx<'tcx> { pub(crate) fn new(tcx: TyCtxt<'tcx>, opts: Options) -> Self { let params_open_inv = gather_params_open_inv(tcx); let creusot_items = creusot_items::local_creusot_items(tcx); @@ -227,6 +228,23 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { self.externs.load(self.tcx, &self.opts.extern_paths); } + /// Fetch the THIR of the given function. + /// + /// If type-checking this function fails, this will return [`CannotFetchThir`], which + /// should then be bubbled up the stack. + pub(crate) fn fetch_thir( + &self, + local_id: LocalDefId, + ) -> Result< + (&'tcx rustc_data_structures::steal::Steal>, thir::ExprId), + CannotFetchThir, + > { + match self.tcx.thir_body(local_id) { + Ok(body) => Ok(body), + Err(_) => Err(CannotFetchThir), + } + } + queryish!(trait_impl, &TraitImpl<'tcx>, translate_impl); queryish!(closure_contract, &ClosureContract<'tcx>, build_closure_contract); @@ -239,25 +257,44 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { self.fmir_body.get(&body_id).unwrap() } - pub(crate) fn term(&mut self, def_id: DefId) -> Option<&Term<'tcx>> { - if !def_id.is_local() { - return self.externs.term(def_id); - } + /// Compute the pearlite term associated with `def_id`. + /// + /// # Returns + /// - `Ok(None)` if `def_id` does not have a body + /// - `Ok(Some(term))` if `def_id` has a body, in this crate or in a dependency. + /// - `Err(CannotFetchThir)` if typechecking the body of `def_id` failed. + pub(crate) fn term(&mut self, def_id: DefId) -> Result>, CannotFetchThir> { + let Some(local_id) = def_id.as_local() else { return Ok(self.externs.term(def_id)) }; - if self.has_body(def_id) { + if self.tcx.hir().maybe_body_owned_by(local_id).is_some() { if !self.terms.contains_key(&def_id) { - let mut term = pearlite::pearlite(self, def_id.expect_local()) - .unwrap_or_else(|e| e.emit(self.tcx)); + let mut term = match pearlite::pearlite(self, local_id) { + Ok(t) => t, + Err(Error::MustPrint(msg)) => msg.emit(self.tcx), + Err(Error::TypeCheck(thir)) => return Err(thir), + }; term = pearlite::normalize(self.tcx, self.param_env(def_id), term); self.terms.insert(def_id, term); }; - self.terms.get(&def_id) + Ok(self.terms.get(&def_id)) } else { - None + Ok(None) } } + /// Same as [`Self::term`], but aborts if an error was found. + /// + /// This should only be used in [`after_analysis`](crate::translation::after_analysis), + /// where we are confident that typechecking errors have already been reported. + pub(crate) fn term_fail_fast(&mut self, def_id: DefId) -> Option<&Term<'tcx>> { + let tcx = self.tcx; + self.term(def_id).unwrap_or_else(|_| { + tcx.dcx().abort_if_errors(); + None + }) + } + pub(crate) fn params_open_inv(&self, def_id: DefId) -> Option<&Vec> { if !def_id.is_local() { return self.externs.params_open_inv(def_id); @@ -271,12 +308,13 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { let body = self.body_with_facts(body_id.def_id); match body_id.promoted { None => &body.body, - Some(promoted) => &body.promoted.get(promoted).unwrap(), + Some(promoted) => body.promoted.get(promoted).unwrap(), } } pub(crate) fn body_with_facts(&mut self, def_id: LocalDefId) -> &BodyWithBorrowckFacts<'tcx> { - if !self.bodies.contains_key(&def_id) { + let entry = self.bodies.entry(def_id); + entry.or_insert_with(|| { let mut body = callbacks::get_body(self.tcx, def_id) .unwrap_or_else(|| panic!("did not find body for {def_id:?}")); @@ -292,10 +330,8 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { } } - self.bodies.insert(def_id, body); - }; - - self.bodies.get(&def_id).unwrap() + body + }) } pub(crate) fn type_invariant( @@ -349,9 +385,9 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { /// We encodes the opacity of functions using 'witnesses', funcitons that have the target opacity /// set as their *visibility*. pub(crate) fn opacity(&mut self, item: DefId) -> &Opacity { - if self.opacity.get(&item).is_none() { + if !self.opacity.contains_key(&item) { self.opacity.insert(item, self.mk_opacity(item)); - }; + } &self.opacity[&item] } @@ -416,7 +452,9 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { self.tcx.hir().maybe_body_owned_by(local_id).is_some() } else { match self.item_type(def_id) { - ItemType::Logic { .. } | ItemType::Predicate { .. } => self.term(def_id).is_some(), + ItemType::Logic { .. } | ItemType::Predicate { .. } => { + matches!(self.term(def_id), Ok(Some(_))) + } _ => false, } } @@ -446,7 +484,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { self.extern_spec_items.insert(def_id, i); for id in c.iter_ids() { - self.term(id).unwrap(); + self.term(id)?.unwrap(); } } } @@ -456,7 +494,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> { self.extern_specs.values().flat_map(|e| e.contract.iter_ids()).collect(); for id in need_to_load { - self.term(id); + self.term(id)?; } for def_id in traits_or_impls { diff --git a/creusot/src/error.rs b/creusot/src/error.rs index a89d71859..4f0dca54c 100644 --- a/creusot/src/error.rs +++ b/creusot/src/error.rs @@ -3,16 +3,21 @@ use rustc_span::{Span, DUMMY_SP}; pub type CreusotResult = Result; +pub(crate) enum Error { + MustPrint(Message), + TypeCheck(CannotFetchThir), +} + // TODO: make this a vector of spans and strings #[derive(Debug)] -pub struct Error { +pub struct Message { span: Span, msg: String, } -impl Error { +impl Message { pub(crate) fn new(span: Span, msg: impl Into) -> Self { - Error { span, msg: msg.into() } + Self { span, msg: msg.into() } } pub(crate) fn emit(self, tcx: TyCtxt) -> ! { @@ -21,12 +26,35 @@ impl Error { } } +impl Error { + pub(crate) fn msg(span: Span, msg: impl Into) -> Self { + Self::MustPrint(Message { span, msg: msg.into() }) + } +} + +impl From for Error { + fn from(value: Message) -> Self { + Self::MustPrint(value) + } +} +impl From for Error { + fn from(value: CannotFetchThir) -> Self { + Self::TypeCheck(value) + } +} + +/// This error is raised when fetching a function's THIR failed, because of a typechecking error. +/// +/// It should usually be bubbled up to the caller, which should then throw it away and +/// proceed to call `tcx.dcx().abort_if_errors()`. +pub(crate) struct CannotFetchThir; + #[derive(Debug, Clone)] pub struct InternalError(pub &'static str); impl From for Error { fn from(err: InternalError) -> Error { - Error::new(DUMMY_SP, format!("internal error: {}", err.0)) + Error::MustPrint(Message::new(DUMMY_SP, format!("internal error: {}", err.0))) } } diff --git a/creusot/src/gather_spec_closures.rs b/creusot/src/gather_spec_closures.rs index f7f3f94fa..6e14e3dfa 100644 --- a/creusot/src/gather_spec_closures.rs +++ b/creusot/src/gather_spec_closures.rs @@ -29,16 +29,16 @@ pub(crate) struct SpecClosures<'tcx> { impl<'tcx> SpecClosures<'tcx> { pub(crate) fn collect(ctx: &mut TranslationCtx<'tcx>, body: &Body<'tcx>) -> Self { let mut visitor = Closures::new(ctx.tcx); - visitor.visit_body(&body); + visitor.visit_body(body); let mut assertions = IndexMap::new(); let mut snapshots = IndexMap::new(); for clos in visitor.closures.into_iter() { if is_assertion(ctx.tcx, clos) { - let term = ctx.term(clos).unwrap().clone(); + let term = ctx.term_fail_fast(clos).unwrap().clone(); assertions.insert(clos, term); } else if is_snapshot_closure(ctx.tcx, clos) { - let term = ctx.term(clos).unwrap().clone(); + let term = ctx.term_fail_fast(clos).unwrap().clone(); snapshots.insert(clos, term); } } @@ -113,7 +113,7 @@ impl<'a, 'tcx> InvariantsVisitor<'a, 'tcx> { if preds.len() > 1 { return Some(block); } - let Some(pred) = preds.get(0) else { + let Some(pred) = preds.first() else { // Reached the top of the function. Impossible. panic!("The impossible happened: Missing 'before_loop' marker."); }; @@ -140,7 +140,7 @@ impl<'a, 'tcx> Visitor<'tcx> for InvariantsVisitor<'a, 'tcx> { } return; }; - let term = self.ctx.term(*id).unwrap().clone(); + let term = self.ctx.term_fail_fast(*id).unwrap().clone(); match self.find_loop_header(loc) { None if let LoopSpecKind::Invariant(expl) = kind => { self.ctx.warn( diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs index 147bca826..6487283db 100644 --- a/creusot/src/translation.rs +++ b/creusot/src/translation.rs @@ -14,7 +14,7 @@ use crate::{ are_contracts_loaded, is_logic, is_no_translate, is_predicate, is_spec, AreContractsLoaded, }, ctx::{self}, - error::InternalError, + error::{Error, InternalError}, metadata, options::Output, translated_item::FileModule, @@ -27,13 +27,13 @@ use ctx::TranslationCtx; use rustc_hir::{def::DefKind, def_id::DefId}; use rustc_middle::ty::TyCtxt; use rustc_span::DUMMY_SP; -use std::{error::Error, fs::File, io::Write, path::PathBuf}; +use std::{fs::File, io::Write, path::PathBuf, time::Instant}; use why3::{ declaration::{Attribute, Decl, Module}, printer::{self, pretty_blocks, Print}, }; -pub(crate) fn before_analysis(ctx: &mut TranslationCtx) -> Result<(), Box> { +pub(crate) fn before_analysis(ctx: &mut TranslationCtx) -> Result<(), Box> { let start = Instant::now(); match are_contracts_loaded(ctx.tcx) { @@ -53,20 +53,29 @@ pub(crate) fn before_analysis(ctx: &mut TranslationCtx) -> Result<(), Box {} + Err(Error::MustPrint(msg)) => msg.emit(ctx.tcx), + Err(Error::TypeCheck(_)) => ctx.tcx.dcx().abort_if_errors(), + }; for def_id in ctx.tcx.hir().body_owners() { - validate_purity(ctx, def_id); + // OK to ignore this error, because we abort after the loop. + let _ = validate_purity(ctx, def_id); let def_id = def_id.to_def_id(); - if is_spec(ctx.tcx, def_id) || is_predicate(ctx.tcx, def_id) || is_logic(ctx.tcx, def_id) { - if !is_trusted_function(ctx.tcx, def_id) { - let _ = ctx.term(def_id); - validate_opacity(ctx, def_id); - } + if (is_spec(ctx.tcx, def_id) || is_predicate(ctx.tcx, def_id) || is_logic(ctx.tcx, def_id)) + && !is_trusted_function(ctx.tcx, def_id) + { + // OK to ignore this error, because we abort after the loop. + let _ = ctx.term(def_id); + let _ = validate_opacity(ctx, def_id); } } - validate_terminates(ctx); + ctx.tcx.dcx().abort_if_errors(); + // OK to ignore this error, because we abort right after. + let _ = validate_terminates(ctx); + ctx.tcx.dcx().abort_if_errors(); // Check that all trait laws are well-formed validate_traits(ctx); @@ -91,9 +100,8 @@ fn should_translate(tcx: TyCtxt, mut def_id: DefId) -> bool { } } -use std::time::Instant; // TODO: Move the main loop out of `translation.rs` -pub(crate) fn after_analysis(ctx: TranslationCtx) -> Result<(), Box> { +pub(crate) fn after_analysis(ctx: TranslationCtx) -> Result<(), Box> { let mut why3 = Why3Generator::new(ctx); let start = Instant::now(); @@ -110,14 +118,17 @@ pub(crate) fn after_analysis(ctx: TranslationCtx) -> Result<(), Box> } info!("Translating body {:?}", def_id); - why3.translate(def_id); + // Ok to ignore, because we call `abort_if_errors` at the end of the next loop + let _ = why3.translate(def_id); } for impls in why3.all_local_trait_impls(()).values() { for impl_id in impls { - why3.translate(impl_id.to_def_id()); + // Ok to ignore, because we call `abort_if_errors` at the end of the loop + let _ = why3.translate(impl_id.to_def_id()); } } + why3.tcx.dcx().abort_if_errors(); debug!("after_analysis_translate: {:?}", start.elapsed()); let start = Instant::now(); @@ -177,9 +188,9 @@ fn show_attribute(attr: &Attribute) -> String { fn modular_output(modl: &FileModule, out: &mut T) -> std::io::Result<()> { let FileModule { path: _, modl: Module { name: _, decls, attrs, meta } } = modl; - let attrs = attrs.into_iter().map(|attr| Decl::Comment(show_attribute(attr))); - let meta = meta.into_iter().map(|s| Decl::Comment(s.clone())); - let decls: Vec = attrs.chain(meta).chain(decls.into_iter().cloned()).collect(); + let attrs = attrs.iter().map(|attr| Decl::Comment(show_attribute(attr))); + let meta = meta.iter().map(|s| Decl::Comment(s.clone())); + let decls: Vec = attrs.chain(meta).chain(decls.iter().cloned()).collect(); pretty_blocks(&decls, &printer::ALLOC).1.render(120, out)?; writeln!(out)?; Ok(()) diff --git a/creusot/src/translation/external.rs b/creusot/src/translation/external.rs index b7389ca07..5b09d8307 100644 --- a/creusot/src/translation/external.rs +++ b/creusot/src/translation/external.rs @@ -1,6 +1,6 @@ use crate::{ ctx::*, - error::{CreusotResult, InternalError}, + error::CreusotResult, translation::{pearlite::Term, specification::ContractClauses, traits}, util::erased_identity_for_item, }; @@ -40,8 +40,7 @@ pub(crate) fn extract_extern_specs_from_item<'tcx>( def_id: LocalDefId, ) -> CreusotResult<(DefId, ExternSpec<'tcx>)> { // Handle error gracefully - let (thir, expr) = - ctx.tcx.thir_body(def_id).map_err(|_| InternalError("Cannot fetch THIR body"))?; + let (thir, expr) = ctx.fetch_thir(def_id)?; let thir = thir.borrow(); let mut visit = ExtractExternItems::new(&thir); diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs index 0afb640b0..1048118c8 100644 --- a/creusot/src/translation/pearlite.rs +++ b/creusot/src/translation/pearlite.rs @@ -16,7 +16,7 @@ use crate::{ get_ghost_inner_logic, get_index_logic, get_snap_inner, is_assertion, is_deref, is_ghost_ty, is_snap_ty, is_spec, }, - error::{CreusotResult, Error, InternalError}, + error::{CannotFetchThir, CreusotResult, Error}, naming::anonymous_param_symbol, translation::{projection_vec::*, TranslationCtx}, }; @@ -285,7 +285,7 @@ pub(crate) fn pearlite<'tcx>( ) -> CreusotResult> { let (triggers, term) = pearlite_with_triggers(ctx, id)?; if !triggers.is_empty() { - Err(Error::new(ctx.def_span(id), TRIGGER_ERROR)) + Err(Error::msg(ctx.def_span(id), TRIGGER_ERROR)) } else { Ok(term) } @@ -295,10 +295,10 @@ pub(crate) fn pearlite_with_triggers<'tcx>( ctx: &TranslationCtx<'tcx>, id: LocalDefId, ) -> CreusotResult<(Vec>, Term<'tcx>)> { - let (thir, expr) = ctx.thir_body(id).map_err(|_| InternalError("Cannot fetch THIR body"))?; + let (thir, expr) = ctx.fetch_thir(id)?; let thir = thir.borrow(); if thir.exprs.is_empty() { - return Err(Error::new(ctx.def_span(id), "type checking failed")); + return Err(Error::TypeCheck(CannotFetchThir)); }; let lower = ThirTerm { ctx, item_id: id, thir: &thir }; @@ -327,15 +327,14 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { self.item_id }; - let (thir, _) = - self.ctx.thir_body(owner_id).map_err(|_| InternalError("Cannot fetch THIR body"))?; + let (thir, _) = self.ctx.fetch_thir(owner_id)?; let thir: &Thir = &thir.borrow(); let res = thir .params .iter() .enumerate() .filter_map(|(idx, param)| { - Some(self.pattern_term(&*param.pat.as_ref()?, true).map(|pat| (idx, param.ty, pat))) + Some(Self::pattern_term(param.pat.as_ref()?, true).map(|pat| (idx, param.ty, pat))) }) .fold_ok(body, |body, (idx, ty, pattern)| match pattern { Pattern::Binder(_) | Pattern::Wildcard => body, @@ -365,7 +364,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { self.collect_triggers(args[1], triggers) } else { let span = self.thir[args[0]].span; - Err(Error::new(span, "Triggers must be tuples")) + Err(Error::msg(span, "Triggers must be tuples")) } } else { Ok(expr) @@ -414,31 +413,31 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { Div => BinOp::Div, Rem => BinOp::Rem, BitXor => { - return Err(Error::new( + return Err(Error::msg( self.thir[expr].span, "bitwise-xors are currently unsupported", )) } BitAnd => { - return Err(Error::new( + return Err(Error::msg( self.thir[expr].span, "bitwise-ands are currently unsupported", )) } BitOr => { - return Err(Error::new( + return Err(Error::msg( self.thir[expr].span, "bitwise-ors are currently unsupported", )) } Shl | ShlUnchecked => { - return Err(Error::new( + return Err(Error::msg( self.thir[expr].span, "shifts are currently unsupported", )) } Shr | ShrUnchecked => { - return Err(Error::new( + return Err(Error::msg( self.thir[expr].span, "shifts are currently unsupported", )) @@ -588,11 +587,11 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { Some(ResultCheck) => { Ok(Term { ty, span, kind: TermKind::Tuple { fields: vec![] } }) } - Some(Dead) => Err(Error::new( + Some(Dead) => Err(Error::msg( span, "The `dead` term can only be used for the body of trusted logical functions", )), - Some(Trigger) => Err(Error::new( + Some(Trigger) => Err(Error::msg( span, "Triggers can only be used directly inside quantifiers", )), @@ -607,7 +606,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { if let Some(new_subst) = is_ghost_box_deref( self.ctx.tcx, id, - subst.get(0).and_then(|arg| arg.as_type()), + subst.first().and_then(|arg| arg.as_type()), ) { let term = self.expr_term(args[0])?; let inner_id = get_ghost_inner_logic(self.ctx.tcx); @@ -741,7 +740,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { TyKind::FnDef(id, substs) => { Ok(Term { ty, span, kind: TermKind::item(*id, substs, user_ty, self.ctx.tcx) }) } - _ => Err(Error::new(thir_term.span, "unhandled literal expression")), + _ => Err(Error::msg(thir_term.span, "unhandled literal expression")), }, ExprKind::NamedConst { def_id, args, ref user_ty, .. } => { Ok(Term { ty, span, kind: TermKind::item(def_id, args, user_ty, self.ctx.tcx) }) @@ -773,35 +772,35 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { let arm = &self.thir[arm]; if arm.guard.is_some() { - return Err(Error::new(arm.span, "match guards are unsupported")); + return Err(Error::msg(arm.span, "match guards are unsupported")); } - let pattern = self.pattern_term(&arm.pattern, false)?; + let pattern = Self::pattern_term(&arm.pattern, false)?; let body = self.expr_term(arm.body)?; Ok((pattern, body)) } - fn pattern_term(&self, pat: &Pat<'tcx>, mut_allowed: bool) -> CreusotResult> { + fn pattern_term(pat: &Pat<'tcx>, mut_allowed: bool) -> CreusotResult> { trace!("{:?}", pat); match &pat.kind { PatKind::Wild => Ok(Pattern::Wildcard), PatKind::Binding { name, mode, .. } => { if mode.0 == ByRef::Yes(Mutability::Mut) { - return Err(Error::new( + return Err(Error::msg( pat.span, "mut ref binders are not supported in pearlite", )); } if !mut_allowed && mode.1 == Mutability::Mut { - return Err(Error::new(pat.span, "mut binders are not supported in pearlite")); + return Err(Error::msg(pat.span, "mut binders are not supported in pearlite")); } Ok(Pattern::Binder(*name)) } PatKind::Variant { subpatterns, adt_def, variant_index, args, .. } => { let mut fields: Vec<_> = subpatterns .iter() - .map(|pat| Ok((pat.field, self.pattern_term(&pat.pattern, mut_allowed)?))) + .map(|pat| Ok((pat.field, Self::pattern_term(&pat.pattern, mut_allowed)?))) .collect::>()?; fields.sort_by_key(|f| f.0); @@ -822,7 +821,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { PatKind::Leaf { subpatterns } => { let mut fields: Vec<_> = subpatterns .iter() - .map(|pat| Ok((pat.field, self.pattern_term(&pat.pattern, mut_allowed)?))) + .map(|pat| Ok((pat.field, Self::pattern_term(&pat.pattern, mut_allowed)?))) .collect::>()?; fields.sort_by_key(|f| f.0); @@ -852,17 +851,17 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { } PatKind::Deref { subpattern } => { if !(pat.ty.is_box() || pat.ty.ref_mutability() == Some(Not)) { - return Err(Error::new( + return Err(Error::msg( pat.span, "only deref patterns for box and & are supported", )); } - self.pattern_term(subpattern, mut_allowed) + Self::pattern_term(subpattern, mut_allowed) } PatKind::Constant { value } => { if !pat.ty.is_bool() { - return Err(Error::new( + return Err(Error::msg( pat.span, "non-boolean constant patterns are unsupported", )); @@ -871,7 +870,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { } // TODO: this simply ignores type annotations, maybe we should actually support them PatKind::AscribeUserType { ascription: _, subpattern } => { - self.pattern_term(subpattern, mut_allowed) + Self::pattern_term(subpattern, mut_allowed) } ref pk => todo!("lower_pattern: unsupported pattern kind {:?}", pk), } @@ -899,7 +898,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { }) } StmtKind::Let { pattern, initializer, init_scope, .. } => { - let pattern = self.pattern_term(pattern, false)?; + let pattern = Self::pattern_term(pattern, false)?; if let Some(initializer) = initializer { let initializer = self.expr_term(*initializer)?; let span = @@ -918,7 +917,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { owner: OwnerId { def_id: self.item_id }, local_id: init_scope.id, }); - Err(Error::new(span, "let-bindings must have values")) + Err(Error::msg(span, "let-bindings must have values")) } } } @@ -936,7 +935,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { Ok((names.to_vec(), pearlite_with_triggers(self.ctx, closure_id)?)) } - _ => Err(Error::new(self.thir[body].span, "unexpected error in quantifier")), + _ => Err(Error::msg(self.thir[body].span, "unexpected error in quantifier")), } } @@ -1037,7 +1036,7 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { let (cur, fin, inner, mut proj) = self.logical_reborrow_inner(args[0])?; if !matches!(self.thir[args[0]].ty.kind(), TyKind::Str | TyKind::Array(_, _) | TyKind::Slice(_)) { - return Err(Error::new( + return Err(Error::msg( span, format!("unsupported logical reborrow of indexing {e:?}, only slice indexing is supported"), )) @@ -1067,10 +1066,10 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> { proj )) } else { - return Err(Error::new(span, format!("unsupported projection {id:?}"))); + Err(Error::msg(span, format!("unsupported projection {id:?}"))) } } - e => Err(Error::new( + e => Err(Error::msg( span, format!("unsupported logical reborrow {e:?}, only field projections and slice indexing are supported"), )), @@ -1090,7 +1089,7 @@ fn is_ghost_box_deref<'tcx>( fn_id: DefId, ty: Option>, ) -> Option<&'tcx GenericArgs<'tcx>> { - let Some(ty) = ty else { return None }; + let ty = ty?; if !is_deref(tcx, fn_id) { return None; } @@ -1106,7 +1105,7 @@ fn is_ghost_box_deref<'tcx>( } } -pub(crate) fn mk_projection<'tcx>(lhs: Term<'tcx>, name: FieldIdx) -> TermKind<'tcx> { +pub(crate) fn mk_projection(lhs: Term, name: FieldIdx) -> TermKind { TermKind::Projection { lhs: Box::new(lhs), name } } @@ -1196,8 +1195,6 @@ pub fn zip_binder<'a, 'tcx>( binder.0.iter().map(|x| x.name).zip(binder.1.tuple_fields()) } -use rustc_hir; - impl<'tcx> Pattern<'tcx> { pub(crate) fn get_bool(&self) -> Option { match self { @@ -1231,45 +1228,43 @@ pub fn super_visit_term<'tcx, V: TermVisitor<'tcx>>(term: &Term<'tcx>, visitor: TermKind::Lit(_) => {} TermKind::Item(_, _) => {} TermKind::Binary { op: _, lhs, rhs } => { - visitor.visit_term(&*lhs); - visitor.visit_term(&*rhs); + visitor.visit_term(lhs); + visitor.visit_term(rhs); } - TermKind::Unary { op: _, arg } => visitor.visit_term(&*arg), + TermKind::Unary { op: _, arg } => visitor.visit_term(arg), TermKind::Quant { body, trigger, .. } => { trigger.iter().flat_map(|x| &x.0).for_each(|x| visitor.visit_term(x)); - visitor.visit_term(&*body) - } - TermKind::Call { id: _, subst: _, args } => { - args.iter().for_each(|a| visitor.visit_term(&*a)) + visitor.visit_term(body) } + TermKind::Call { id: _, subst: _, args } => args.iter().for_each(|a| visitor.visit_term(a)), TermKind::Constructor { typ: _, variant: _, fields } => { - fields.iter().for_each(|a| visitor.visit_term(&*a)) + fields.iter().for_each(|a| visitor.visit_term(a)) } - TermKind::Tuple { fields } => fields.iter().for_each(|a| visitor.visit_term(&*a)), - TermKind::Cur { term } => visitor.visit_term(&*term), - TermKind::Fin { term } => visitor.visit_term(&*term), + TermKind::Tuple { fields } => fields.iter().for_each(|a| visitor.visit_term(a)), + TermKind::Cur { term } => visitor.visit_term(term), + TermKind::Fin { term } => visitor.visit_term(term), TermKind::Impl { lhs, rhs } => { - visitor.visit_term(&*lhs); - visitor.visit_term(&*rhs) + visitor.visit_term(lhs); + visitor.visit_term(rhs) } TermKind::Match { scrutinee, arms } => { - visitor.visit_term(&*scrutinee); - arms.iter().for_each(|(_, arm)| visitor.visit_term(&*arm)) + visitor.visit_term(scrutinee); + arms.iter().for_each(|(_, arm)| visitor.visit_term(arm)) } TermKind::Let { pattern: _, arg, body } => { - visitor.visit_term(&*arg); - visitor.visit_term(&*body) + visitor.visit_term(arg); + visitor.visit_term(body) } - TermKind::Projection { lhs, name: _ } => visitor.visit_term(&*lhs), - TermKind::Old { term } => visitor.visit_term(&*term), - TermKind::Closure { body, .. } => visitor.visit_term(&*body), + TermKind::Projection { lhs, name: _ } => visitor.visit_term(lhs), + TermKind::Old { term } => visitor.visit_term(term), + TermKind::Closure { body, .. } => visitor.visit_term(body), TermKind::Reborrow { cur, fin, inner, projection } => { - visitor.visit_term(&*cur); - visitor.visit_term(&*fin); - visitor.visit_term(&*inner); + visitor.visit_term(cur); + visitor.visit_term(fin); + visitor.visit_term(inner); visit_projections(projection, |term| visitor.visit_term(term)) } - TermKind::Assert { cond } => visitor.visit_term(&*cond), + TermKind::Assert { cond } => visitor.visit_term(cond), } } @@ -1496,7 +1491,7 @@ impl<'tcx> Term<'tcx> { } pub(crate) fn subst_with Option>>(&mut self, mut f: F) { - self.subst_with_inner(&mut HashSet::new(), &mut f) + self.subst_with_inner(&HashSet::new(), &mut f) } fn subst_with_inner Option>>( @@ -1509,9 +1504,8 @@ impl<'tcx> Term<'tcx> { if bound.contains(v) { return; } - match inv_subst(*v) { - Some(t) => self.kind = t.kind.clone(), - None => (), + if let Some(t) = inv_subst(*v) { + self.kind = t.kind.clone() } } TermKind::Lit(_) => {} @@ -1673,11 +1667,7 @@ impl Display for PrintExpr<'_, '_> { } #[allow(dead_code)] -fn print_thir_expr<'tcx>( - fmt: &mut Formatter, - thir: &Thir<'tcx>, - expr_id: ExprId, -) -> std::fmt::Result { +fn print_thir_expr(fmt: &mut Formatter, thir: &Thir, expr_id: ExprId) -> std::fmt::Result { match &thir[expr_id].kind { ExprKind::Call { fun, args, .. } => { print_thir_expr(fmt, thir, *fun)?; diff --git a/creusot/src/translation/specification.rs b/creusot/src/translation/specification.rs index d8fd5b9f8..96172862b 100644 --- a/creusot/src/translation/specification.rs +++ b/creusot/src/translation/specification.rs @@ -134,7 +134,7 @@ impl ContractClauses { let n_requires = self.requires.len(); for req_id in self.requires { log::trace!("require clause {:?}", req_id); - let term = ctx.term(req_id).unwrap().clone(); + let term = ctx.term_fail_fast(req_id).unwrap().clone(); let expl = if n_requires == 1 { format!("expl:{} requires", fn_name) } else { @@ -146,7 +146,7 @@ impl ContractClauses { let n_ensures = self.ensures.len(); for ens_id in self.ensures { log::trace!("ensures clause {:?}", ens_id); - let term = ctx.term(ens_id).unwrap().clone(); + let term = ctx.term_fail_fast(ens_id).unwrap().clone(); let expl = if n_ensures == 1 { format!("expl:{} ensures", fn_name) } else { @@ -157,7 +157,7 @@ impl ContractClauses { if let Some(var_id) = self.variant { log::trace!("variant clause {:?}", var_id); - let term = ctx.term(var_id).unwrap().clone(); + let term = ctx.term_fail_fast(var_id).unwrap().clone(); out.variant = Some(term); }; log::trace!("no_panic: {}", self.no_panic); @@ -226,10 +226,10 @@ impl<'tcx> ScopeTree<'tcx> { while let Some(s) = to_visit.take() { let d = (HashSet::new(), None); - self.0.get(&s).unwrap_or_else(|| &d).0.iter().for_each(|(id, loc)| { + self.0.get(&s).unwrap_or(&d).0.iter().for_each(|(id, loc)| { locals.entry(*id).or_insert(*loc); }); - to_visit = self.0.get(&s).unwrap_or_else(|| &d).1.clone(); + to_visit = self.0.get(&s).unwrap_or(&d).1; } locals @@ -257,7 +257,7 @@ pub(crate) fn inv_subst<'tcx>( /// Translate a place to a term. The place must represent a single named variable, so it can be /// - A simple `mir::Local`. /// - A capture. In this case, the place will simply be a local (the capture's envirnoment) -/// followed by +/// followed by /// + a `Deref` projection if the closure is FnMut. /// + a `Field` projection. /// + a `Deref` projection if the capture is mutable. @@ -470,7 +470,7 @@ pub(crate) fn pre_sig_of<'tcx>( unnest_subst, vec![Term::var(self_, env_ty).cur(), Term::var(self_, env_ty).fin()], ); - let expl = format!("expl:closure unnest"); + let expl = "expl:closure unnest".to_string(); contract.ensures.push(Condition { term, expl }); }; @@ -576,10 +576,7 @@ pub(crate) fn pre_sig_of<'tcx>( PreSignature { inputs, output, contract } } -fn inputs_and_output<'tcx>( - tcx: TyCtxt<'tcx>, - def_id: DefId, -) -> (impl Iterator)>, Ty<'tcx>) { +fn inputs_and_output(tcx: TyCtxt, def_id: DefId) -> (impl Iterator, Ty) { let ty = tcx.type_of(def_id).instantiate_identity(); let (inputs, output): (Box>, _) = match ty .kind() diff --git a/creusot/src/validate.rs b/creusot/src/validate.rs index c41e2c066..6d4fcc74c 100644 --- a/creusot/src/validate.rs +++ b/creusot/src/validate.rs @@ -15,7 +15,7 @@ use crate::{ is_spec, is_trusted, opacity_witness_name, }, ctx::TranslationCtx, - error::{Error, InternalError}, + error::CannotFetchThir, pearlite::{pearlite_stub, Stub}, specification::contract_of, traits::TraitResolved, @@ -36,7 +36,10 @@ pub(crate) fn validate_trusted(ctx: &mut TranslationCtx) { } } -pub(crate) fn validate_opacity(ctx: &mut TranslationCtx, item: DefId) -> Option<()> { +pub(crate) fn validate_opacity( + ctx: &mut TranslationCtx, + item: DefId, +) -> Result<(), CannotFetchThir> { struct OpacityVisitor<'a, 'tcx> { ctx: &'a TranslationCtx<'tcx>, opacity: Option, @@ -86,11 +89,11 @@ pub(crate) fn validate_opacity(ctx: &mut TranslationCtx, item: DefId) -> Option< } if is_spec(ctx.tcx, item) { - return Some(()); + return Ok(()); } // UGLY clone... - let term = ctx.term(item)?.clone(); + let Some(term) = ctx.term(item)?.cloned() else { return Ok(()) }; if ctx.visibility(item) != Visibility::Restricted(parent_module(ctx.tcx, item)) && opacity_witness_name(ctx.tcx, item).is_none() @@ -100,7 +103,7 @@ pub(crate) fn validate_opacity(ctx: &mut TranslationCtx, item: DefId) -> Option< let opacity = ctx.opacity(item).scope(); OpacityVisitor { opacity, ctx, source_item: item }.visit_term(&term); - Some(()) + Ok(()) } // Validate that laws have no additional generic parameters. @@ -287,26 +290,32 @@ impl Purity { } } -pub(crate) fn validate_purity(ctx: &mut TranslationCtx, def_id: LocalDefId) { - let (thir, expr) = ctx - .thir_body(def_id) - .unwrap_or_else(|_| Error::from(InternalError("Cannot fetch THIR body")).emit(ctx.tcx)); +pub(crate) fn validate_purity( + ctx: &mut TranslationCtx, + def_id: LocalDefId, +) -> Result<(), CannotFetchThir> { + let (thir, expr) = ctx.fetch_thir(def_id)?; let thir = thir.borrow(); if thir.exprs.is_empty() { - Error::new(ctx.def_span(def_id), "type checking failed").emit(ctx.tcx); + // TODO: put this inside `fetch_thir`? + return Err(CannotFetchThir); } let def_id = def_id.to_def_id(); let purity = Purity::of_def_id(ctx, def_id); if matches!(purity, Purity::Program { .. }) && is_no_translate(ctx.tcx, def_id) { - return; + return Ok(()); } let param_env = ctx.tcx.param_env(def_id); - thir::visit::walk_expr( - &mut PurityVisitor { ctx, thir: &thir, context: purity, param_env }, - &thir[expr], - ); + let mut visitor = + PurityVisitor { ctx, thir: &thir, context: purity, param_env, thir_failed: false }; + thir::visit::walk_expr(&mut visitor, &thir[expr]); + if visitor.thir_failed { + Err(CannotFetchThir) + } else { + Ok(()) + } } struct PurityVisitor<'a, 'tcx> { @@ -315,6 +324,8 @@ struct PurityVisitor<'a, 'tcx> { context: Purity, /// Typing environment of the caller function param_env: ParamEnv<'tcx>, + // If `true`, we should error with a [`CannotFetchThir`] error. + thir_failed: bool, } impl<'a, 'tcx> PurityVisitor<'a, 'tcx> { @@ -395,20 +406,24 @@ impl<'a, 'tcx> thir::visit::Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> { return; } - let (thir, expr) = self.ctx.thir_body(closure_id).unwrap_or_else(|_| { - Error::from(InternalError("Cannot fetch THIR body")).emit(self.ctx.tcx) - }); + let Ok((thir, expr)) = self.ctx.thir_body(closure_id) else { + self.thir_failed = true; + return; + }; let thir = thir.borrow(); - thir::visit::walk_expr( - &mut PurityVisitor { - ctx: self.ctx, - thir: &thir, - context: self.context, - param_env: self.param_env, - }, - &thir[expr], - ); + let mut visitor = PurityVisitor { + ctx: self.ctx, + thir: &thir, + context: self.context, + param_env: self.param_env, + thir_failed: false, + }; + thir::visit::walk_expr(&mut visitor, &thir[expr]); + if visitor.thir_failed { + self.thir_failed = true; + return; + } } _ => {} } diff --git a/creusot/src/validate_terminates.rs b/creusot/src/validate_terminates.rs index fccb654d4..e62fcc215 100644 --- a/creusot/src/validate_terminates.rs +++ b/creusot/src/validate_terminates.rs @@ -37,6 +37,7 @@ use crate::{ has_variant_clause, is_ghost_closure, is_ghost_from_fn, is_no_translate, is_pearlite, }, ctx::TranslationCtx, + error::CannotFetchThir, pearlite::{TermKind, TermVisitor}, specification::contract_of, traits::TraitResolved, @@ -58,15 +59,15 @@ use rustc_trait_selection::traits::normalize_param_env_or_error; /// Validate that a `#[terminates]` function cannot loop indefinitely. This includes: /// - forbidding program function from using loops of any kind (this should be relaxed -/// later). +/// later). /// - forbidding (mutual) recursive calls, especially when traits are involved. /// /// Note that for logical functions, these are relaxed: we don't check loops, nor simple /// recursion, because why3 will handle it for us. -pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) { +pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) -> Result<(), CannotFetchThir> { ctx.tcx.dcx().abort_if_errors(); // There may have been errors before, if a `#[terminates]` calls a non-`#[terminates]`. - let CallGraph { graph: mut call_graph, additional_data } = CallGraph::build(ctx); + let CallGraph { graph: mut call_graph, additional_data } = CallGraph::build(ctx)?; // Detect simple recursion, and loops for fun_index in call_graph.node_indices() { @@ -157,7 +158,7 @@ pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) { let last = idx == cycle.len(); if let Some(e) = call_graph.edges_connecting(current_node, next_node).next() { let call = *e.weight(); - let adverb = if last && cycle.len() >= 1 { "finally" } else { "then" }; + let adverb = if last && !cycle.is_empty() { "finally" } else { "then" }; let punct = if last { "." } else { "..." }; let f1 = ctx.tcx.def_path_str(call_graph.node_weight(current_node).unwrap().def_id()); @@ -185,6 +186,7 @@ pub(crate) fn validate_terminates(ctx: &mut TranslationCtx) { } ctx.tcx.dcx().abort_if_errors(); + Ok(()) } struct CallGraph { @@ -317,7 +319,7 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { called_id: DefId, generic_args: GenericArgsRef<'tcx>, call_span: Span, - ) { + ) -> Result<(), CannotFetchThir> { let tcx = ctx.tcx; let (called_id, generic_args) = if TraitResolved::is_trait_item(tcx, called_id) { match TraitResolved::resolve_item(tcx, param_env, called_id, generic_args) { @@ -337,7 +339,7 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { let ghost_node = self.insert_function(tcx, GraphNode::Function(*ghost_def_id)); self.graph.update_edge(node, ghost_node, CallKind::Ghost); - return; + return Ok(()); } // TODO: this code is kind of a soup, rework or refactor into a function @@ -374,7 +376,7 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { default_function: called_id, impl_block: spec_impl_id, }; - let Some(node) = self.visit_specialized_default_function(ctx, default_node) else { + let Some(node) = self.visit_specialized_default_function(ctx, default_node)? else { break 'not_default; }; let bounds = self.default_functions_bounds[&node]; @@ -415,6 +417,7 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { ); } } + Ok(()) } /// This visit the special function that is called when calling: @@ -437,10 +440,14 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { &mut self, ctx: &mut TranslationCtx<'tcx>, graph_node: ImplDefaultTransparent, - ) -> Option { - let node = *self.graph_node_to_index.get(&GraphNode::ImplDefaultTransparent(graph_node))?; + ) -> Result, CannotFetchThir> { + let Some(&node) = + self.graph_node_to_index.get(&GraphNode::ImplDefaultTransparent(graph_node)) + else { + return Ok(None); + }; if !self.visited_default_specialization.insert(node) { - return Some(node); + return Ok(Some(node)); } let tcx = ctx.tcx; let ImplDefaultTransparent { default_function: item_id, impl_block: impl_id } = graph_node; @@ -448,7 +455,7 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { let impl_id = impl_id.to_def_id(); let param_env = tcx.param_env(impl_id); - let term = ctx.term(item_id).unwrap(); + let term = ctx.term(item_id)?.unwrap(); let mut visitor = TermCalls { results: IndexSet::new() }; visitor.visit_term(term); @@ -484,9 +491,9 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { EarlyBinder::bind(generic_args), ); - self.function_call(ctx, node, param_env, called_id, actual_args, call_span); + self.function_call(ctx, node, param_env, called_id, actual_args, call_span)?; } - Some(node) + Ok(Some(node)) } } @@ -495,7 +502,7 @@ impl CallGraph { /// exclusively for the purpose of termination checking. /// /// In particular, this means it only contains `#[terminates]` functions. - fn build(ctx: &mut TranslationCtx) -> Self { + fn build(ctx: &mut TranslationCtx) -> Result { let tcx = ctx.tcx; let mut build_call_graph = BuildFunctionsGraph::default(); @@ -569,10 +576,19 @@ impl CallGraph { let (thir, expr) = ctx.thir_body(local_id).unwrap(); let thir = thir.borrow(); // Collect functions called by this function - let mut visitor = - FunctionCalls { thir: &thir, tcx, calls: IndexSet::new(), has_loops: None }; + let mut visitor = FunctionCalls { + thir: &thir, + tcx, + calls: IndexSet::new(), + has_loops: None, + thir_failed: false, + }; ::visit_expr(&mut visitor, &thir[expr]); + if visitor.thir_failed { + return Err(CannotFetchThir); + } + build_call_graph.additional_data[&node].has_loops = visitor.has_loops; for (called_id, generic_args, call_span) in visitor.calls { @@ -583,11 +599,14 @@ impl CallGraph { called_id, generic_args, call_span, - ); + )?; } } - Self { graph: build_call_graph.graph, additional_data: build_call_graph.additional_data } + Ok(Self { + graph: build_call_graph.graph, + additional_data: build_call_graph.additional_data, + }) } } @@ -602,6 +621,8 @@ struct FunctionCalls<'thir, 'tcx> { calls: IndexSet<(DefId, &'tcx GenericArgs<'tcx>, Span)>, /// `Some` if the function contains a loop construct. has_loops: Option, + /// If `true`, we should error with a [`CannotFetchThir`] error. + thir_failed: bool, } impl<'thir, 'tcx> thir::visit::Visitor<'thir, 'tcx> for FunctionCalls<'thir, 'tcx> { @@ -617,10 +638,10 @@ impl<'thir, 'tcx> thir::visit::Visitor<'thir, 'tcx> for FunctionCalls<'thir, 'tc } } thir::ExprKind::Closure(box thir::ClosureExpr { closure_id, .. }) => { - let (thir, expr) = self.tcx.thir_body(closure_id).unwrap_or_else(|_| { - crate::error::Error::from(crate::error::InternalError("Cannot fetch THIR body")) - .emit(self.tcx) - }); + let Ok((thir, expr)) = self.tcx.thir_body(closure_id) else { + self.thir_failed = true; + return; + }; let thir = thir.borrow(); let mut closure_visitor = FunctionCalls { @@ -628,8 +649,13 @@ impl<'thir, 'tcx> thir::visit::Visitor<'thir, 'tcx> for FunctionCalls<'thir, 'tc tcx: self.tcx, calls: std::mem::take(&mut self.calls), has_loops: None, + thir_failed: false, }; thir::visit::walk_expr(&mut closure_visitor, &thir[expr]); + if closure_visitor.thir_failed { + self.thir_failed = true; + return; + } self.calls.extend(closure_visitor.calls); self.has_loops = self.has_loops.or(closure_visitor.has_loops); } diff --git a/creusot/tests/should_fail/array.stderr b/creusot/tests/should_fail/array.stderr index a293ca296..c0950e6c4 100644 --- a/creusot/tests/should_fail/array.stderr +++ b/creusot/tests/should_fail/array.stderr @@ -10,7 +10,5 @@ error: Unsupported expression: Repeat 13 | #[requires([0; 4] == x)] | ^^^^^^ -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors diff --git a/creusot/tests/should_fail/diagnostics/add_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/add_unimplemented.stderr index 01b2dacef..8e6180ce3 100644 --- a/creusot/tests/should_fail/diagnostics/add_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/add_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: Cannot add `i32` to `i32` in logic = help: the trait `creusot_contracts::logic::ops::AddLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::AddLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/div_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/div_unimplemented.stderr index 45664c967..6681f2a30 100644 --- a/creusot/tests/should_fail/diagnostics/div_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/div_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: Cannot divide `i32` by `i32` in logic = help: the trait `creusot_contracts::logic::ops::DivLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::DivLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/index_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/index_unimplemented.stderr index cd3e64dc8..0d9323a41 100644 --- a/creusot/tests/should_fail/diagnostics/index_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/index_unimplemented.stderr @@ -12,8 +12,6 @@ error[E0599]: no method named `index_logic` found for struct `S` in the current candidate #1: `creusot_contracts::logic::ops::IndexLogic` = note: this error originates in the attribute macro `logic` (in Nightly builds, run with -Z macro-backtrace for more info) -error: internal error: Cannot fetch THIR body - -error: aborting due to 2 previous errors +error: aborting due to 1 previous error For more information about this error, try `rustc --explain E0599`. diff --git a/creusot/tests/should_fail/diagnostics/mul_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/mul_unimplemented.stderr index 65db425a2..b64d56939 100644 --- a/creusot/tests/should_fail/diagnostics/mul_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/mul_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: Cannot multiply `i32` by `i32` in logic = help: the trait `creusot_contracts::logic::ops::MulLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::MulLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/neg_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/neg_unimplemented.stderr index e9cebb84b..352b211c3 100644 --- a/creusot/tests/should_fail/diagnostics/neg_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/neg_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: cannot apply unary operator `-` to type `i32` = help: the trait `creusot_contracts::logic::ops::NegLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::NegLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/rem_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/rem_unimplemented.stderr index d528fdc4d..7eb868a10 100644 --- a/creusot/tests/should_fail/diagnostics/rem_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/rem_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: cannot calculate the remainder of `i32` divided by `i32` in logic = help: the trait `creusot_contracts::logic::ops::RemLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::RemLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/sub_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/sub_unimplemented.stderr index 5f8b3c2da..d35cf3838 100644 --- a/creusot/tests/should_fail/diagnostics/sub_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/sub_unimplemented.stderr @@ -19,8 +19,6 @@ error[E0277]: Cannot subtract `i32` from `i32` in logic = help: the trait `creusot_contracts::logic::ops::SubLogic` is not implemented for `i32` = help: the trait `creusot_contracts::logic::ops::SubLogic` is implemented for `creusot_contracts::Int` -error: internal error: Cannot fetch THIR body - -error: aborting due to 3 previous errors +error: aborting due to 2 previous errors For more information about this error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/diagnostics/view_unimplemented.rs b/creusot/tests/should_fail/diagnostics/view_unimplemented.rs index 3d78f330a..5c61fe293 100644 --- a/creusot/tests/should_fail/diagnostics/view_unimplemented.rs +++ b/creusot/tests/should_fail/diagnostics/view_unimplemented.rs @@ -7,8 +7,9 @@ struct S; #[logic] fn views(x: S) { let _ = x.view(); +} + +fn view_operator(x: S) { // FIXME(diagnostics): this error is printed twice, why? let _ = pearlite! { x@ }; } - -// FIXME(diagnostics): separating this into 2 functions causes the second one to be ignored. We probably have an early exit that is a bit too eager (Look into the "Cannot fetch THIR body" error). diff --git a/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr b/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr index 15b406d9b..7c2f27fcf 100644 --- a/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr +++ b/creusot/tests/should_fail/diagnostics/view_unimplemented.stderr @@ -22,9 +22,9 @@ note: the trait `creusot_contracts::View` must be implemented candidate #1: `creusot_contracts::View` error[E0277]: Cannot take the model of `S` - --> view_unimplemented.rs:11:25 + --> view_unimplemented.rs:14:25 | -11 | let _ = pearlite! { x@ }; +14 | let _ = pearlite! { x@ }; | ^- | | | no implementation for `S@` @@ -43,9 +43,9 @@ error[E0277]: Cannot take the model of `S` and 32 others error[E0277]: Cannot take the model of `S` - --> view_unimplemented.rs:11:25 + --> view_unimplemented.rs:14:25 | -11 | let _ = pearlite! { x@ }; +14 | let _ = pearlite! { x@ }; | ^^ no implementation for `S@` | = help: the trait `creusot_contracts::View` is not implemented for `S` @@ -60,9 +60,7 @@ error[E0277]: Cannot take the model of `S` creusot_contracts::Snapshot and 32 others -error: internal error: Cannot fetch THIR body - -error: aborting due to 4 previous errors +error: aborting due to 3 previous errors Some errors have detailed explanations: E0277, E0599. For more information about an error, try `rustc --explain E0277`. diff --git a/creusot/tests/should_fail/non_bool_assertion.stderr b/creusot/tests/should_fail/non_bool_assertion.stderr index 1a0729a8b..e6d9baeee 100644 --- a/creusot/tests/should_fail/non_bool_assertion.stderr +++ b/creusot/tests/should_fail/non_bool_assertion.stderr @@ -10,8 +10,6 @@ error[E0308]: mismatched types = help: consider constraining the associated type `::ViewTy` to `bool` = note: for more information, visit https://doc.rust-lang.org/book/ch19-03-advanced-traits.html -error: internal error: Cannot fetch THIR body - -error: aborting due to 2 previous errors +error: aborting due to 1 previous error For more information about this error, try `rustc --explain E0308`. diff --git a/creusot/tests/should_fail/unsupported/macros.stderr b/creusot/tests/should_fail/unsupported/macros.stderr index c2e3aa76d..78198e2ac 100644 --- a/creusot/tests/should_fail/unsupported/macros.stderr +++ b/creusot/tests/should_fail/unsupported/macros.stderr @@ -4,7 +4,5 @@ error: Unsupported expression: macros other than `pearlite!` or `proof_assert!` 7 | panic!() | ^^^^^^^^ -error: internal error: Cannot fetch THIR body - -error: aborting due to 2 previous errors +error: aborting due to 1 previous error