diff --git a/cli/driver/src/callbacks_wrapper.rs b/cli/driver/src/callbacks_wrapper.rs index 6cd97895e..3fa124373 100644 --- a/cli/driver/src/callbacks_wrapper.rs +++ b/cli/driver/src/callbacks_wrapper.rs @@ -22,12 +22,12 @@ impl<'a> Callbacks for CallbacksWrapper<'a> { })); self.sub.config(config) } - fn after_parsing<'tcx>( + fn after_crate_root_parsing<'tcx>( &mut self, compiler: &interface::Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { - self.sub.after_parsing(compiler, queries) + self.sub.after_crate_root_parsing(compiler, queries) } fn after_expansion<'tcx>( &mut self, @@ -38,10 +38,9 @@ impl<'a> Callbacks for CallbacksWrapper<'a> { } fn after_analysis<'tcx>( &mut self, - early_handler: &rustc_session::EarlyErrorHandler, compiler: &interface::Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { - self.sub.after_analysis(early_handler, compiler, queries) + self.sub.after_analysis(compiler, queries) } } diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index 4e023d31a..948fbf5b5 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -287,7 +287,7 @@ impl From for hax_frontend_exporter_options::Options { } impl Callbacks for ExtractionCallbacks { - fn after_parsing<'tcx>( + fn after_crate_root_parsing<'tcx>( &mut self, compiler: &Compiler, queries: &'tcx Queries<'tcx>, diff --git a/cli/driver/src/linter.rs b/cli/driver/src/linter.rs index beb286f07..ba82517f8 100644 --- a/cli/driver/src/linter.rs +++ b/cli/driver/src/linter.rs @@ -16,7 +16,7 @@ impl LinterCallbacks { } impl Callbacks for LinterCallbacks { - fn after_parsing<'tcx>( + fn after_crate_root_parsing<'tcx>( &mut self, _compiler: &Compiler, queries: &'tcx Queries<'tcx>, diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 6505c83a7..bf4f5c323 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1064,7 +1064,7 @@ end) : EXPR = struct let c_clause_kind span id (kind : Thir.clause_kind) : impl_ident option = match kind with - | Trait { is_positive = true; is_const = _; trait_ref } -> + | Trait { is_positive = true; trait_ref } -> let args = List.map ~f:(c_generic_value span) trait_ref.generic_args in let trait = Concrete_ident.of_def_id Trait trait_ref.def_id in Some { goal = { trait; args }; name = id } @@ -1301,13 +1301,13 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = let c_body = if drop_body then c_expr_drop_body else c_expr in (* TODO: things might be unnamed (e.g. constants) *) match (item.kind : Thir.item_kind) with - | Const (_, body) -> + | Const (_, generics, body) -> mk @@ Fn { name = Concrete_ident.of_def_id Value (Option.value_exn item.def_id); - generics = { params = []; constraints = [] }; + generics = c_generics generics; body = c_body body; params = []; } diff --git a/flake.lock b/flake.lock index b5435ed81..836a2c82b 100644 --- a/flake.lock +++ b/flake.lock @@ -120,10 +120,7 @@ "fstar": "fstar", "hacl-star": "hacl-star", "nixpkgs": "nixpkgs", - "rust-overlay": [ - "crane", - "rust-overlay" - ] + "rust-overlay": "rust-overlay_2" } }, "rust-overlay": { @@ -151,6 +148,29 @@ "type": "github" } }, + "rust-overlay_2": { + "inputs": { + "flake-utils": [ + "flake-utils" + ], + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1716862669, + "narHash": "sha256-7oTPM9lcdwiI1cpRC313B+lHawocgpY5F07N+Rbm5Uk=", + "owner": "oxalica", + "repo": "rust-overlay", + "rev": "47b2d15658b37716393b2463a019000dbd6ce4bc", + "type": "github" + }, + "original": { + "owner": "oxalica", + "repo": "rust-overlay", + "type": "github" + } + }, "systems": { "locked": { "lastModified": 1681028828, diff --git a/flake.nix b/flake.nix index 4c331088a..522c67996 100644 --- a/flake.nix +++ b/flake.nix @@ -8,7 +8,11 @@ flake-utils.follows = "flake-utils"; }; }; - rust-overlay.follows = "crane/rust-overlay"; + rust-overlay = { + url = "github:oxalica/rust-overlay"; + inputs.flake-utils.follows = "flake-utils"; + inputs.nixpkgs.follows = "nixpkgs"; + }; fstar = { url = "github:FStarLang/FStar/v2024.01.13"; inputs = { diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index a02f4c86f..6c99bb3d9 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -1,4 +1,5 @@ use crate::prelude::*; +use rustc_middle::{mir, ty}; #[derive( Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, @@ -188,7 +189,6 @@ pub(crate) fn scalar_int_to_constant_literal<'tcx, S: UnderOwnerState<'tcx>>( x: rustc_middle::ty::ScalarInt, ty: rustc_middle::ty::Ty, ) -> ConstantLiteral { - use rustc_middle::ty; match ty.kind() { ty::Char => ConstantLiteral::Char( char::try_from(x) @@ -222,7 +222,6 @@ pub(crate) fn scalar_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>( span: rustc_span::Span, ) -> ConstantExpr { use rustc_middle::mir::Mutability; - use rustc_middle::ty; let cspan = span.sinto(s); // The documentation explicitly says not to match on a scalar. // We match on the type and use it to convert the value. @@ -388,21 +387,23 @@ pub trait ConstantExt<'tcx>: Sized + std::fmt::Debug { } } } -impl<'tcx> ConstantExt<'tcx> for rustc_middle::ty::Const<'tcx> { +impl<'tcx> ConstantExt<'tcx> for ty::Const<'tcx> { fn eval_constant>(&self, s: &S) -> Option { - let evaluated = self.eval(s.base().tcx, s.param_env()); + let evaluated = self.eval(s.base().tcx, s.param_env(), None).ok()?; + let evaluated = ty::Const::new(s.base().tcx, ty::ConstKind::Value(evaluated), self.ty()); (&evaluated != self).then_some(evaluated) } } -impl<'tcx> ConstantExt<'tcx> for rustc_middle::mir::ConstantKind<'tcx> { +impl<'tcx> ConstantExt<'tcx> for mir::ConstantKind<'tcx> { fn eval_constant>(&self, s: &S) -> Option { - let evaluated = self.eval(s.base().tcx, s.param_env()); + let evaluated = self.eval(s.base().tcx, s.param_env(), None).ok()?; + let evaluated = mir::ConstantKind::Val(evaluated, self.ty()); (&evaluated != self).then_some(evaluated) } } -impl<'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_middle::ty::Const<'tcx> { +impl<'tcx, S: UnderOwnerState<'tcx>> SInto for ty::Const<'tcx> { fn sinto(&self, s: &S) -> ConstantExpr { - use rustc_middle::{query::Key, ty}; + use rustc_middle::query::Key; let span = self.default_span(s.base().tcx); let kind = match self.kind() { ty::ConstKind::Param(p) => ConstantExprKind::ConstRef { id: p.sinto(s) }, @@ -434,7 +435,6 @@ pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>( ty: rustc_middle::ty::Ty<'tcx>, span: rustc_span::Span, ) -> ConstantExpr { - use rustc_middle::ty; let kind = match (valtree, ty.kind()) { (_, ty::Ref(_, inner_ty, _)) => { ConstantExprKind::Borrow(valtree_to_constant_expr(s, valtree, *inner_ty, span)) @@ -537,7 +537,7 @@ pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>( use rustc_middle::mir::interpret::ConstValue; match val { ConstValue::Scalar(scalar) => scalar_to_constant_expr(s, ty, &scalar, span), - ConstValue::ByRef { .. } => const_value_reference_to_constant_expr(s, ty, val, span), + ConstValue::Indirect { .. } => const_value_reference_to_constant_expr(s, ty, val, span), ConstValue::Slice { data, start, end } => { let start = start.try_into().unwrap(); let end = end.try_into().unwrap(); diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs index 71b4ae887..2b70d4df9 100644 --- a/frontend/exporter/src/state.rs +++ b/frontend/exporter/src/state.rs @@ -143,8 +143,8 @@ mod types { macro_infos: Rc::new(HashMap::new()), cached_thirs: Rc::new(HashMap::new()), options: Rc::new(options), - /// Always prefer `s.owner_id()` to `s.base().opt_def_id`. - /// `opt_def_id` is used in `utils` for error reporting + // Always prefer `s.owner_id()` to `s.base().opt_def_id`. + // `opt_def_id` is used in `utils` for error reporting opt_def_id: None, local_ctx: Rc::new(RefCell::new(LocalContextS::new())), exported_spans: Rc::new(RefCell::new(HashSet::new())), diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index cae1cec9c..30497a5d3 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -130,8 +130,8 @@ pub(crate) mod search_clause { let erase_and_norm = |x| tcx.erase_regions(tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x)); // Lifetime and constantness are irrelevant when resolving instances - let x = erase_and_norm(x).without_const(tcx); - let y = erase_and_norm(y).without_const(tcx); + let x = erase_and_norm(x); + let y = erase_and_norm(y); let sx = format!("{:?}", x.kind().skip_binder()); let sy = format!("{:?}", y.kind().skip_binder()); let result = sx == sy; @@ -324,7 +324,7 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> { generics: generics.sinto(s), } .with_args(impl_exprs(s, &nested), trait_ref), - ImplSource::Param(nested, _constness) => { + ImplSource::Param(nested) => { use search_clause::TraitPredicateExt; let tcx = s.base().tcx; let predicates = &tcx.predicates_defined_on_or_above(s.owner_id()); @@ -362,22 +362,19 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> { .with_args(impl_exprs(s, &nested), trait_ref) } } - ImplSource::Object(data) => { - ImplExprAtom::Dyn.with_args(impl_exprs(s, &data.nested), trait_ref) - } // We ignore the contained obligations here. For example for `(): Send`, the // obligations contained would be `[(): Send]`, which leads to an infinite loop. There // might be important obligation shere inother cases; we'll have to see if that comes // up. - ImplSource::Builtin(_ignored) => ImplExprAtom::Builtin { - r#trait: self.skip_binder().sinto(s), + ImplSource::Builtin(source, _ignored) => { + let atom = match source { + BuiltinImplSource::Object { .. } => ImplExprAtom::Dyn, + _ => ImplExprAtom::Builtin { + r#trait: self.skip_binder().sinto(s), + }, + }; + atom.with_args(vec![], trait_ref) } - .with_args(vec![], trait_ref), - x => ImplExprAtom::Todo(format!( - "ImplExprAtom::Todo(see https://github.com/hacspec/hax/issues/381) {:#?}\n\n{:#?}", - x, self - )) - .with_args(vec![], trait_ref), } } } diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index f85fe9783..7b61f17bb 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -461,6 +461,7 @@ pub enum CanonicalVarInfo { PlaceholderRegion(PlaceholderRegion), Const(UniverseIndex, Ty), PlaceholderConst(PlaceholderConst, Ty), + Effect, } /// Reflects [`rustc_middle::ty::UserSelfTy`] @@ -1031,18 +1032,6 @@ pub struct Stmt { pub opt_destruction_scope: Option, } -/// Reflects [`rustc_ast::ast::MacDelimiter`] -#[derive(AdtInto)] -#[args(, from: rustc_ast::ast::MacDelimiter, state: S as _s)] -#[derive( - Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, -)] -pub enum MacDelimiter { - Parenthesis, - Bracket, - Brace, -} - /// Reflects [`rustc_ast::token::Delimiter`] #[derive(AdtInto)] #[args(, from: rustc_ast::token::Delimiter, state: S as _s)] @@ -1164,7 +1153,7 @@ pub struct Token { )] pub struct DelimArgs { pub dspan: DelimSpan, - pub delim: MacDelimiter, + pub delim: Delimiter, pub tokens: TokenStream, } @@ -1602,7 +1591,8 @@ impl Alias { // emit a warning with a lot of debugging information. let poly_trait_ref = if trait_ref.has_escaping_bound_vars() { let trait_ref_and_generics = alias_ty.trait_ref_and_own_args(tcx); - let rebased_generics = alias_ty.rebase_args_onto_impl(alias_ty.args, tcx); + let rebased_generics = + alias_ty.rebase_inherent_args_onto_impl(alias_ty.args, tcx); let norm_rebased_generics = tcx.try_subst_and_normalize_erasing_regions( rebased_generics, s.param_env(), @@ -2845,7 +2835,6 @@ pub struct Impl { pub polarity: ImplPolarity, pub defaultness: Defaultness, pub defaultness_span: Option, - pub constness: Constness, pub generics: Generics, #[map({ s.base().tcx.impl_trait_ref(s.owner_id()).sinto(s) @@ -3031,7 +3020,7 @@ pub enum ItemKind { ExternCrate(Option), Use(UsePath, UseKind), Static(Ty, Mutability, Body), - Const(Ty, Body), + Const(Ty, Generics, Body), #[custom_arm( rustc_hir::ItemKind::Fn(sig, generics, body) => { ItemKind::Fn(generics.sinto(s), make_fn_def::(sig, body, s)) @@ -3229,9 +3218,6 @@ pub struct TraitRef { )] pub struct TraitPredicate { pub trait_ref: TraitRef, - #[from(constness)] - #[map(x.clone() == rustc_middle::ty::BoundConstness::ConstIfConst)] - pub is_const: bool, #[map(x.clone() == rustc_middle::ty::ImplPolarity::Positive)] #[from(polarity)] pub is_positive: bool, diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 06e3d3031..97c19eaae 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -529,8 +529,6 @@ pub enum TerminatorKind { discr: Operand, targets: SwitchTargets, }, - Resume, - Terminate, Return, Unreachable, Drop { @@ -581,6 +579,8 @@ pub enum TerminatorKind { real_target: BasicBlock, unwind: UnwindAction, }, + UnwindResume, + UnwindTerminate(UnwindTerminateReason), InlineAsm { template: Vec, operands: Vec, @@ -734,7 +734,7 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto // of the the state captured by a closure. use crate::rustc_index::Idx; let generics = generics.as_closure(); - let upvar_tys: Vec<_> = generics.upvar_tys().collect(); + let upvar_tys = generics.upvar_tys(); current_ty = upvar_tys[index.sinto(s).index()].clone(); ProjectionElem::Field(ProjectionElemFieldKind::ClosureState( index.sinto(s), diff --git a/frontend/exporter/src/types/mod.rs b/frontend/exporter/src/types/mod.rs index 64c149415..bc679676d 100644 --- a/frontend/exporter/src/types/mod.rs +++ b/frontend/exporter/src/types/mod.rs @@ -1,3 +1,6 @@ +// There's a conflict between `mir::ScalarInt`and `todo::ScalarInt` but it doesn't matter. +#![allow(ambiguous_glob_reexports)] + mod copied; mod index; mod mir; diff --git a/frontend/exporter/src/types/todo.rs b/frontend/exporter/src/types/todo.rs index 2a52aa1dd..6df174278 100644 --- a/frontend/exporter/src/types/todo.rs +++ b/frontend/exporter/src/types/todo.rs @@ -7,6 +7,7 @@ sinto_todo!(rustc_abi, IntegerType); sinto_todo!(rustc_abi, ReprFlags); sinto_todo!(rustc_abi, Align); sinto_todo!(rustc_middle::mir::interpret, ConstAllocation<'a>); +sinto_todo!(rustc_middle::mir, UnwindTerminateReason); sinto_todo!(rustc_ast::tokenstream, DelimSpan); sinto_todo!(rustc_hir::def, DefKind); sinto_todo!(rustc_hir, GenericArgs<'a> as HirGenericArgs); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 794fd61a1..7dee8050a 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-07-15" +channel = "nightly-2023-09-19" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 24a197840..8047ce566 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -243,7 +243,7 @@ class t_Lang (v_Self: Type0) = { } class t_SuperTrait (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_10391689928755043351:Core.Clone.t_Clone v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self; f_function_of_super_trait_pre:v_Self -> bool; f_function_of_super_trait_post:v_Self -> u32 -> bool; f_function_of_super_trait:x0: v_Self @@ -255,7 +255,7 @@ class t_SuperTrait (v_Self: Type0) = { [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_SuperTrait_for_i32: t_SuperTrait i32 = { - _super_10391689928755043351 = FStar.Tactics.Typeclasses.solve; + _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; f_function_of_super_trait_pre = (fun (self: i32) -> true); f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true); f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32 @@ -263,8 +263,8 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 = class t_Foo (v_Self: Type0) = { f_AssocType:Type0; - f_AssocType_1566547207180513319:t_SuperTrait f_AssocType; - f_AssocType_18427724250319916167:Core.Clone.t_Clone f_AssocType; + f_AssocType_17663802186765685673:t_SuperTrait f_AssocType; + f_AssocType_10139459042277121690:Core.Clone.t_Clone f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> bool; f_assoc_f_post:Prims.unit -> Prims.unit -> bool; @@ -315,7 +315,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x let impl_Foo_for_tuple_: t_Foo Prims.unit = { f_AssocType = i32; - f_AssocType_1566547207180513319 = FStar.Tactics.Typeclasses.solve; + f_AssocType_17663802186765685673 = FStar.Tactics.Typeclasses.solve; f_N = sz 32; f_assoc_f_pre = (fun (_: Prims.unit) -> true); f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);