diff --git a/README.md b/README.md index 0d3ddccd53..b666890ef6 100644 --- a/README.md +++ b/README.md @@ -15,4 +15,7 @@ For an overview, take a look at the [`flux` website](https://flux-rs.github.io). # Docs Documentation, including installation and usage guides can be found on the -[website](https://flux-rs.github.io/flux). \ No newline at end of file +[website](https://flux-rs.github.io/flux). + + +TRACE: insert_fn_sig DefId(0:14 ~ maps00[5caf]::rmap::{impl#0}::new) fn() -> {a0:RMap. RMap[K, V][a0] | true} \ No newline at end of file diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index 3ab1132f4d..a8f2a5c537 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -3,10 +3,9 @@ use std::{borrow::Borrow, iter}; use flux_common::{bug, index::IndexGen, iter::IterExt, span_bug}; use flux_errors::FluxSession; use flux_middle::{ - fhir::{self, lift::LiftCtxt, ExprKind, FhirId, FluxOwnerId, Res}, + fhir::{self, lift::LiftCtxt, ExprKind, FhirId, FluxOwnerId, GenericParamKind, Res}, global_env::GlobalEnv, intern::List, - rty::GenericParamDefKind, }; use flux_syntax::surface; use hir::{def::DefKind, ItemKind, PrimTy}; @@ -234,6 +233,7 @@ impl<'a, 'tcx> DesugarCtxt<'a, 'tcx> { let kind = match ¶m.kind { surface::GenericParamKind::Type => fhir::GenericParamKind::Type { default: None }, surface::GenericParamKind::Base => fhir::GenericParamKind::BaseTy, + surface::GenericParamKind::Spl => fhir::GenericParamKind::SplTy, surface::GenericParamKind::Refine { .. } => { continue; } @@ -1633,7 +1633,7 @@ fn index_sort( resolver_output: &ResolverOutput, bty: &surface::BaseTy, ) -> Option { - // CODESYNC(sort-of, 4) sorts should be given consistently + // CODESYNC(sort-of, 3) sorts should be given consistently match &bty.kind { surface::BaseTyKind::Path(path) => sort_of_surface_path(genv, resolver_output, path), surface::BaseTyKind::Slice(_) => Some(fhir::Sort::Int), @@ -1645,8 +1645,7 @@ fn sort_of_surface_path( resolver_output: &ResolverOutput, path: &surface::Path, ) -> Option { - // CODESYNC(sort-of, 4) sorts should be given consistently - + // CODESYNC(sort-of-path, 2) sorts should be given consistently let res = resolver_output.path_res_map[&path.node_id]; match res { @@ -1655,25 +1654,27 @@ fn sort_of_surface_path( fhir::Res::PrimTy(PrimTy::Float(..) | PrimTy::Str | PrimTy::Char) => Some(fhir::Sort::Unit), fhir::Res::Def(DefKind::TyAlias { .. } | DefKind::Enum | DefKind::Struct, def_id) => { // TODO: duplication with sort_of_path - let Ok(generics) = genv.generics_of(def_id) else { return None }; let mut sort_args = vec![]; - for (param, arg) in generics.params.iter().zip(&path.generics) { - if param.kind == GenericParamDefKind::BaseTy { - let surface::GenericArg::Type(ty) = arg else { return None }; - let surface::BaseTyKind::Path(path) = &ty.as_bty()?.kind else { - return None; - }; - let sort = sort_of_surface_path(genv, resolver_output, path)?; - sort_args.push(sort); + if let Some(generics) = genv.map().get_generics(def_id) { + for (param, arg) in generics.params.iter().zip(&path.generics) { + if let GenericParamKind::SplTy = param.kind { + let surface::GenericArg::Type(ty) = arg else { return None }; + let surface::BaseTyKind::Path(path) = &ty.as_bty()?.kind else { + return None; + }; + let sort = sort_of_surface_path(genv, resolver_output, path)?; + sort_args.push(sort); + } } - } - println!("TRACE: sort_of_surface_path: {def_id:?} {sort_args:?}"); + }; Some(fhir::Sort::Record(def_id, List::from_vec(sort_args))) } fhir::Res::Def(DefKind::TyParam, def_id) => { let param = genv.get_generic_param(def_id.expect_local()); match ¶m.kind { - fhir::GenericParamKind::BaseTy => Some(fhir::Sort::Param(def_id)), + fhir::GenericParamKind::BaseTy | fhir::GenericParamKind::SplTy => { + Some(fhir::Sort::Param(def_id)) + } fhir::GenericParamKind::Type { .. } | fhir::GenericParamKind::Lifetime => None, } } diff --git a/crates/flux-desugar/src/lib.rs b/crates/flux-desugar/src/lib.rs index fce9fedbb6..8ea41caa70 100644 --- a/crates/flux-desugar/src/lib.rs +++ b/crates/flux-desugar/src/lib.rs @@ -53,14 +53,7 @@ pub fn desugar_struct_def( let mut cx = DesugarCtxt::new(genv, owner_id, resolver_output, None); // Desugar and insert generics - let (generics, predicates) = if let Some(generics) = &struct_def.generics { - (cx.desugar_generics(generics)?, cx.as_lift_cx().lift_predicates()?) - } else { - cx.as_lift_cx().lift_generics_with_predicates()? - }; - let refined_by = genv.map().refined_by(owner_id.def_id); - let generics = generics.with_refined_by(refined_by); - genv.map().insert_generics(def_id, generics); + let predicates = cx.as_lift_cx().lift_predicates()?; // Desugar of struct_def needs to happen AFTER inserting generics. See #generics-and-desugaring let struct_def = cx.desugar_struct_def(struct_def, &mut Binders::new())?; diff --git a/crates/flux-driver/src/callbacks.rs b/crates/flux-driver/src/callbacks.rs index 3f7c3ed5dc..fa237c2f67 100644 --- a/crates/flux-driver/src/callbacks.rs +++ b/crates/flux-driver/src/callbacks.rs @@ -153,10 +153,11 @@ fn stage1_desugar(genv: &mut GlobalEnv, specs: &Specs) -> Result<(), ErrorGuaran .err() .or(err); - // Register RefinedBys + // Register RefinedBys (for structs and enums, which also registers their Generics) err = specs .refined_bys() .try_for_each_exhaust(|(owner_id, refined_by)| { + let generics = lift::lift_generics(tcx, sess, owner_id)?; let refined_by = if let Some(refined_by) = refined_by { let def_id = owner_id.to_def_id(); let generics = tcx.generics_of(def_id); @@ -164,6 +165,7 @@ fn stage1_desugar(genv: &mut GlobalEnv, specs: &Specs) -> Result<(), ErrorGuaran } else { lift::lift_refined_by(tcx, owner_id) }; + map.insert_generics(owner_id.def_id, generics.with_refined_by(&refined_by)); map.insert_refined_by(owner_id.def_id, refined_by); Ok(()) }) diff --git a/crates/flux-fhir-analysis/src/conv.rs b/crates/flux-fhir-analysis/src/conv.rs index ed9a289294..1bc3ef38a8 100644 --- a/crates/flux-fhir-analysis/src/conv.rs +++ b/crates/flux-fhir-analysis/src/conv.rs @@ -162,6 +162,7 @@ pub(crate) fn conv_generics( fhir::GenericParamKind::Type { default } => { rty::GenericParamDefKind::Type { has_default: default.is_some() } } + fhir::GenericParamKind::SplTy => rty::GenericParamDefKind::SplTy, fhir::GenericParamKind::BaseTy => rty::GenericParamDefKind::BaseTy, fhir::GenericParamKind::Lifetime => rty::GenericParamDefKind::Lifetime, }; @@ -395,8 +396,9 @@ impl<'a, 'tcx> ConvCtxt<'a, 'tcx> { let kind = rty::BoundRegionKind::BrNamed(def_id.to_def_id(), name); Ok(rty::BoundVariableKind::Region(kind)) } - fhir::GenericParamKind::Type { default: _ } => bug!("unexpected!"), - fhir::GenericParamKind::BaseTy => bug!("unexpected!"), + fhir::GenericParamKind::Type { default: _ } + | fhir::GenericParamKind::BaseTy + | fhir::GenericParamKind::SplTy => bug!("unexpected!"), } } @@ -635,6 +637,9 @@ impl<'a, 'tcx> ConvCtxt<'a, 'tcx> { fn conv_base_ty(&self, env: &mut Env, bty: &fhir::BaseTy) -> QueryResult { let sort = self.genv.sort_of_bty(bty); + // if sort.is_none() { + // println!("TRACE: conv_base_ty {bty:?} ==> None"); + // } if let fhir::BaseTyKind::Path(fhir::QPath::Resolved(self_ty, path)) = &bty.kind { if let fhir::Res::Def(DefKind::AssocTy, def_id) = path.res { diff --git a/crates/flux-fhir-analysis/src/lib.rs b/crates/flux-fhir-analysis/src/lib.rs index 95814ecf14..93046bbc0f 100644 --- a/crates/flux-fhir-analysis/src/lib.rs +++ b/crates/flux-fhir-analysis/src/lib.rs @@ -160,7 +160,7 @@ fn generics_of(genv: &GlobalEnv, local_id: LocalDefId) -> QueryResult Wf<'a, 'tcx> { ) -> Result<(), ErrorGuaranteed> { if let Some(def_id) = adt_id && let Ok(generics) = self.genv.generics_of(def_id) - //&& - // let Some(local_def_id) = def_id.as_local() { - // let refined_by = self.genv.map().refined_by(local_def_id); for (arg, param) in args.iter().zip(generics.params.iter()) { - // if refined_by.is_base_generic(param.def_id) { - if param.kind == GenericParamDefKind::BaseTy { + if param.kind == GenericParamDefKind::SplTy { if let fhir::GenericArg::Type(ty) = arg { self.check_ty_is_base(ty)? } diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index 209eb2845c..ccc0dd95d3 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -35,76 +35,6 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> { } } - // CUT - // pub(super) fn check_refine_params( - // &mut self, - // owner_id: OwnerId, - // refine_params: &[fhir::RefineParam], - // ) -> Result<(), ErrorGuaranteed> { - // let allowed_generics: HashSet = self - // .genv - // .generics_of(owner_id) - // .emit(self.genv.sess)? - // .params - // .iter() - // .filter_map(|param| { - // if let GenericParamDefKind::BaseTy = param.kind { - // Some(param.def_id) - // } else { - // None - // } - // }) - // .collect(); - // println!("TRACE: check_refine_params {owner_id:?} {allowed_generics:?} {refine_params:?}"); - // for refine_param in refine_params { - // self.check_sort(&allowed_generics, &refine_param.sort)? - // } - // Ok(()) - // } - - // CUT - // fn check_sort( - // &self, - // allowed_generics: &HashSet, - // sort: &fhir::Sort, - // ) -> Result<(), ErrorGuaranteed> { - // match sort { - // fhir::Sort::Int - // | fhir::Sort::Bool - // | fhir::Sort::Real - // | fhir::Sort::Loc - // | fhir::Sort::Unit - // | fhir::Sort::BitVec(_) - // | fhir::Sort::Var(_) - // | fhir::Sort::Infer(_) - // | fhir::Sort::Wildcard => Ok(()), - // fhir::Sort::App(_, sorts) => { - // for sort in sorts { - // self.check_sort(allowed_generics, sort)?; - // } - // Ok(()) - // } - // fhir::Sort::Func(poly_func_sort) => { - // for sort in &poly_func_sort.skip_binders().inputs_and_output { - // self.check_sort(allowed_generics, sort)?; - // } - // Ok(()) - // } - // fhir::Sort::Record(_, sorts) => { - // for sort in sorts { - // self.check_sort(allowed_generics, sort)?; - // } - // Ok(()) - // } - // fhir::Sort::Param(def_id) => { - // if allowed_generics.contains(def_id) { - // Ok(()) - // } else { - // Err(self.emit_err(errors::InvalidGenericSort::new(span, sort))) - // } - // } - // } - // } pub(super) fn check_refine_arg( &mut self, arg: &fhir::RefineArg, @@ -278,6 +208,7 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> { } fhir::ExprKind::Dot(var, fld) => { let sort = self[var.name].clone(); + // println!("TRACE: synth_expr {:?} ==> {sort:?}", var.source_info.name); match &sort { fhir::Sort::Record(def_id, sort_args) => { self.genv diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index 9344bbf05d..0b19d70298 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -65,6 +65,7 @@ pub struct GenericParam { #[derive(Debug)] pub enum GenericParamKind { Type { default: Option }, + SplTy, BaseTy, Lifetime, } @@ -144,7 +145,7 @@ type Cache = elsa::FrozenMap>, + generics: Cache>, predicates: ItemPredicates, opaque_tys: UnordMap, func_decls: FxHashMap, @@ -791,7 +792,7 @@ impl Generics { let mut params = vec![]; for param in self.params { let kind = if refined_by.is_base_generic(param.def_id.to_def_id()) { - GenericParamKind::BaseTy + GenericParamKind::SplTy } else { param.kind }; @@ -1090,7 +1091,7 @@ impl Map { } pub fn insert_generics(&self, def_id: LocalDefId, generics: Generics) { - self.generics.insert(def_id, Box::new(generics)); + self.generics.insert(def_id.to_def_id(), Box::new(generics)); } pub fn insert_generic_predicates(&mut self, def_id: LocalDefId, predicates: GenericPredicates) { @@ -1101,7 +1102,7 @@ impl Map { self.opaque_tys.extend_unord(opaque_tys.into_items()); } - pub fn get_generics(&self, def_id: LocalDefId) -> Option<&Generics> { + pub fn get_generics(&self, def_id: DefId) -> Option<&Generics> { self.generics.get(&def_id) } diff --git a/crates/flux-middle/src/fhir/lift.rs b/crates/flux-middle/src/fhir/lift.rs index 51986dc62b..4ab6f11c18 100644 --- a/crates/flux-middle/src/fhir/lift.rs +++ b/crates/flux-middle/src/fhir/lift.rs @@ -33,6 +33,14 @@ pub fn lift_refined_by(tcx: TyCtxt, owner_id: OwnerId) -> fhir::RefinedBy { } } +pub fn lift_generics<'a, 'tcx>( + tcx: TyCtxt<'tcx>, + sess: &'a FluxSession, + owner_id: OwnerId, +) -> Result { + LiftCtxt::new(tcx, sess, owner_id, None).lift_generics() +} + pub fn lift_type_alias( tcx: TyCtxt, sess: &FluxSession, diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs index 8d4304b963..c16306995e 100644 --- a/crates/flux-middle/src/global_env.rs +++ b/crates/flux-middle/src/global_env.rs @@ -13,7 +13,7 @@ pub use rustc_span::{symbol::Ident, Symbol}; use crate::{ cstore::CrateStoreDyn, - fhir::{self, FluxLocalDefId, VariantIdx}, + fhir::{self, FluxLocalDefId, GenericParamKind, VariantIdx}, intern::List, queries::{Providers, Queries, QueryResult}, rty::{self, fold::TypeFoldable, normalize::Defns, refining::Refiner}, @@ -159,7 +159,10 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { pub fn get_generic_param(&self, def_id: LocalDefId) -> &fhir::GenericParam { let owner = self.hir().ty_param_owner(def_id); - self.map().get_generics(owner).unwrap().get_param(def_id) + self.map() + .get_generics(owner.to_def_id()) + .unwrap() + .get_param(def_id) } pub fn is_box(&self, res: fhir::Res) -> bool { @@ -202,6 +205,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { } pub fn sort_of_path(&self, path: &fhir::Path) -> Option { + // CODESYNC(sort-of-path, 2) sorts should be given consistently match path.res { fhir::Res::PrimTy(PrimTy::Int(_) | PrimTy::Uint(_)) => Some(fhir::Sort::Int), fhir::Res::PrimTy(PrimTy::Bool) => Some(fhir::Sort::Bool), @@ -210,13 +214,15 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { } fhir::Res::Def(DefKind::TyAlias { .. } | DefKind::Enum | DefKind::Struct, def_id) => { let mut sort_args = vec![]; - for arg in &path.args { - if let fhir::GenericArg::Type(ty) = arg && - let Some(sort) = self.sort_of_ty(ty) - { - sort_args.push(sort); + if let Some(generics) = self.map().get_generics(def_id) { + for (param, arg) in generics.params.iter().zip(&path.args) { + if let GenericParamKind::SplTy = param.kind { + let fhir::GenericArg::Type(ty) = arg else { return None }; + let sort = self.sort_of_ty(ty)?; + sort_args.push(sort); + } } - } + }; Some(fhir::Sort::Record(def_id, List::from_vec(sort_args))) } fhir::Res::SelfTyAlias { alias_to, .. } => self.sort_of_self_ty_alias(alias_to), @@ -235,7 +241,9 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { fn sort_of_generic_param(&self, def_id: DefId) -> Option { let param = self.get_generic_param(def_id.expect_local()); match ¶m.kind { - fhir::GenericParamKind::BaseTy => Some(fhir::Sort::Param(def_id)), + fhir::GenericParamKind::BaseTy | fhir::GenericParamKind::SplTy => { + Some(fhir::Sort::Param(def_id)) + } fhir::GenericParamKind::Type { .. } | fhir::GenericParamKind::Lifetime => None, } } @@ -259,7 +267,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { fn sort_of_self_ty(&self, def_id: DefId, ty: rustc_middle::ty::Ty) -> Option { use rustc_middle::ty; - // CODESYNC(sort-of, 4) sorts should be given consistently + // CODESYNC(sort-of, 3) sorts should be given consistently match ty.kind() { ty::TyKind::Bool => Some(fhir::Sort::Bool), ty::TyKind::Slice(_) | ty::TyKind::Int(_) | ty::TyKind::Uint(_) => { diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index dd96f7853d..bddeba6b33 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -83,6 +83,7 @@ pub struct GenericParamDef { #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum GenericParamDefKind { Type { has_default: bool }, + SplTy, BaseTy, Lifetime, Const { has_default: bool }, @@ -438,10 +439,19 @@ impl GenericArg { bug!("expected `rty::GenericArg::Ty`, found {:?}", self) } } + pub fn is_valid_base_arg(&self) -> bool { + let res = match self { + GenericArg::Ty(ty) => ty.kind().is_valid_base_ty(), + GenericArg::BaseTy(bty) => bty.skip_binder_as_ref().kind().is_valid_base_ty(), + _ => false, + }; + // println!("TRACE: is_valid_base arg: {:?} => {res:?}", self); + res + } fn from_param_def(param: &GenericParamDef) -> Self { match param.kind { - GenericParamDefKind::Type { .. } => { + GenericParamDefKind::Type { .. } | GenericParamDefKind::SplTy => { let param_ty = ParamTy { index: param.index, name: param.name }; GenericArg::Ty(Ty::param(param_ty)) } @@ -771,6 +781,10 @@ impl Binder { self.value } + pub fn skip_binder_as_ref(&self) -> &T { + &self.value + } + pub fn rebind(self, value: U) -> Binder { Binder { vars: self.vars, value } } @@ -1296,6 +1310,19 @@ impl TyKind { fn intern(self) -> Ty { Interned::new(TyS { kind: self }) } + + fn is_valid_base_ty(&self) -> bool { + match self { + TyKind::Param(_) | TyKind::Indexed(_, _) | TyKind::Exists(_) => true, + TyKind::Constr(_, ty) => ty.kind().is_valid_base_ty(), + TyKind::Uninit + | TyKind::Ptr(_, _) + | TyKind::Discr(_, _) + | TyKind::Downcast(_, _, _, _, _) + | TyKind::Blocked(_) + | TyKind::Alias(_, _) => false, + } + } } impl TyS { @@ -1468,7 +1495,7 @@ impl BaseTy { } pub fn sort(&self) -> Sort { - // CODESYNC(sort-of, 4) sorts should be given consistently + // CODESYNC(sort-of, 3) sorts should be given consistently match self { BaseTy::Int(_) | BaseTy::Uint(_) | BaseTy::Slice(_) => Sort::Int, BaseTy::Bool => Sort::Bool, diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index 5e00f3fba6..4853de11e8 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -231,6 +231,9 @@ impl<'a, 'tcx> Refiner<'a, 'tcx> { (rty::GenericParamDefKind::Type { .. }, rustc::ty::GenericArg::Ty(ty)) => { Ok(rty::GenericArg::Ty(self.refine_ty(ty)?)) } + (rty::GenericParamDefKind::SplTy, rustc::ty::GenericArg::Ty(ty)) => { + Ok(rty::GenericArg::Ty(self.refine_ty(ty)?)) + } (rty::GenericParamDefKind::BaseTy, rustc::ty::GenericArg::Ty(ty)) => { Ok(rty::GenericArg::BaseTy(self.refine_poly_ty(ty)?)) } @@ -320,7 +323,7 @@ impl<'a, 'tcx> Refiner<'a, 'tcx> { } rustc::ty::TyKind::Param(param_ty) => { match self.param(*param_ty)?.kind { - rty::GenericParamDefKind::Type { .. } => { + rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::SplTy => { return Ok(rty::Binder::new(rty::Ty::param(*param_ty), List::empty())); } rty::GenericParamDefKind::BaseTy => rty::BaseTy::Param(*param_ty), diff --git a/crates/flux-refineck/locales/en-US.ftl b/crates/flux-refineck/locales/en-US.ftl index 35f93c1cc1..4909a54da7 100644 --- a/crates/flux-refineck/locales/en-US.ftl +++ b/crates/flux-refineck/locales/en-US.ftl @@ -28,6 +28,9 @@ refineck_assert_error = refineck_param_inference_error = parameter inference error at function call +refineck_invalid_generic_arg = + cannot instantiate base or spl generic with opaque type + refineck_fold_error = type invariant may not hold (when place is folded) diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 098385fe6b..865e95ae49 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -1342,6 +1342,7 @@ pub(crate) mod errors { Inference, OpaqueStruct(DefId), Query(QueryErr), + InvalidGenericArg, } impl CheckerError { @@ -1363,6 +1364,12 @@ pub(crate) mod errors { flux_errors::diagnostic_id(), ) } + CheckerErrKind::InvalidGenericArg => { + handler.struct_err_with_code( + fluent::refineck_invalid_generic_arg, + flux_errors::diagnostic_id(), + ) + } CheckerErrKind::OpaqueStruct(def_id) => { let mut builder = handler.struct_err_with_code( fluent::refineck_opaque_struct_error, diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index d603be8333..874974ca89 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -9,8 +9,9 @@ use flux_middle::{ evars::{EVarCxId, EVarSol, UnsolvedEvar}, fold::TypeFoldable, AliasTy, BaseTy, BinOp, Binder, Const, Constraint, ESpan, EVarGen, EarlyBinder, Expr, - ExprKind, FnOutput, GeneratorObligPredicate, GenericArg, GenericArgs, HoleKind, InferMode, - Mutability, Path, PolyFnSig, PolyVariant, PtrKind, Ref, Sort, TupleTree, Ty, TyKind, Var, + ExprKind, FnOutput, GeneratorObligPredicate, GenericArg, GenericArgs, GenericParamDefKind, + HoleKind, InferMode, Mutability, Path, PolyFnSig, PolyVariant, PtrKind, Ref, Sort, + TupleTree, Ty, TyKind, Var, }, rustc::mir::{BasicBlock, Place}, }; @@ -146,6 +147,26 @@ impl<'a, 'tcx> ConstrGen<'a, 'tcx> { Ok(res) } + fn check_generic_args( + &self, + did: DefId, + generic_args: &[GenericArg], + ) -> Result<(), CheckerErrKind> { + let generics = self.genv.generics_of(did)?; + for (idx, arg) in generic_args.iter().enumerate() { + let param = generics.param_at(idx, self.genv)?; + match param.kind { + GenericParamDefKind::SplTy | GenericParamDefKind::BaseTy => { + if !arg.is_valid_base_arg() { + return Err(CheckerErrKind::InvalidGenericArg); + } + } + _ => continue, + } + } + Ok(()) + } + #[allow(clippy::too_many_arguments)] pub(crate) fn check_fn_call( &mut self, @@ -184,6 +205,10 @@ impl<'a, 'tcx> ConstrGen<'a, 'tcx> { let callsite_def_id = self.def_id; let span = self.span; + if let Some(did) = callee_def_id { + self.check_generic_args(did, generic_args)?; + } + let mut infcx = self.infcx(rcx, ConstrReason::Call); let snapshot = rcx.snapshot(); @@ -698,7 +723,7 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> { } } (GenericArg::BaseTy(_), GenericArg::BaseTy(_)) => { - tracked_span_bug!("sgeneric argument subtyping for base types is not implemented"); + tracked_span_bug!("generic argument subtyping for base types is not implemented"); } (GenericArg::Lifetime(_), GenericArg::Lifetime(_)) => Ok(()), _ => tracked_span_bug!("incompatible generic args: `{arg1:?}` `{arg2:?}"), diff --git a/crates/flux-syntax/src/grammar.lalrpop b/crates/flux-syntax/src/grammar.lalrpop index 939afe9b36..944355db0e 100644 --- a/crates/flux-syntax/src/grammar.lalrpop +++ b/crates/flux-syntax/src/grammar.lalrpop @@ -25,6 +25,7 @@ GenericParam: surface::GenericParam = { let kind = match kind.as_str() { "type" => surface::GenericParamKind::Type, "base" => surface::GenericParamKind::Base, + "spl" => surface::GenericParamKind::Spl, _ => return Err(ParseError::User { error: UserParseError::UnexpectedToken(lo, hi) }) }; Ok(surface::GenericParam { name, kind }) diff --git a/crates/flux-syntax/src/surface.rs b/crates/flux-syntax/src/surface.rs index 4d8775ac48..9b1c440a80 100644 --- a/crates/flux-syntax/src/surface.rs +++ b/crates/flux-syntax/src/surface.rs @@ -60,6 +60,7 @@ pub struct GenericParam { #[derive(Debug)] pub enum GenericParamKind { Type, + Spl, Base, Refine { sort: Sort }, } diff --git a/crates/flux-tests/tests/lib/rmap.rs b/crates/flux-tests/tests/lib/rmap.rs index 7dc175b203..8f74fbc6ef 100644 --- a/crates/flux-tests/tests/lib/rmap.rs +++ b/crates/flux-tests/tests/lib/rmap.rs @@ -9,7 +9,7 @@ use std::hash::Hash; /// define a type indexed by a map #[flux::opaque] -#[flux::refined_by(map: Map)] +#[flux::refined_by(vals: Map)] pub struct RMap { inner: std::collections::HashMap, } @@ -17,12 +17,15 @@ pub struct RMap { #[flux::generics(K as base, V as base)] impl RMap { #[flux::trusted] + + /// #[flux::sig(fn() -> RMap{m: true})] "OK" i.e. wraps K, V in existential + /// #[flux::sig(fn() -> RMap{m: true})] "CRASH" i.e. wraps K, V in LAMBDA pub fn new() -> Self { Self { inner: std::collections::HashMap::new() } } #[flux::trusted] - #[flux::sig(fn(self: &strg RMap[@m], k: K, v: V) ensures self: RMap[map_set(m, k, v)])] + #[flux::sig(fn(self: &strg RMap[@m], k: K, v: V) ensures self: RMap[map_set(m.vals, k, v)])] pub fn set(&mut self, k: K, v: V) where K: Eq + Hash, @@ -31,11 +34,11 @@ impl RMap { } #[flux::trusted] - #[flux::sig(fn(&RMap[@m], &K[@k]) -> Option<&V[map_get(m, k)]>)] + #[flux::sig(fn(&RMap[@m], &K[@k]) -> Option<&V[map_get(m.vals, k)]>)] pub fn get(&self, k: &K) -> Option<&V> where K: Eq + Hash, { - self.inner.get(&k) + self.inner.get(k) } } diff --git a/crates/flux-tests/tests/lib/rset.rs b/crates/flux-tests/tests/lib/rset.rs index 109122fd7e..5a57195125 100644 --- a/crates/flux-tests/tests/lib/rset.rs +++ b/crates/flux-tests/tests/lib/rset.rs @@ -8,6 +8,7 @@ pub struct RSet { pub inner: std::collections::HashSet, } +// TODO: (RJ) I get some odd error with `T as spl` ...? #[flux::generics(T as base)] impl RSet { #[flux::trusted] diff --git a/crates/flux-tests/tests/neg/error_messages/wf/kinds00.rs b/crates/flux-tests/tests/neg/error_messages/wf/kinds00.rs index 652651c1b2..012a6e4b69 100644 --- a/crates/flux-tests/tests/neg/error_messages/wf/kinds00.rs +++ b/crates/flux-tests/tests/neg/error_messages/wf/kinds00.rs @@ -13,14 +13,3 @@ pub fn test00_bad() -> RSet { //~^ ERROR values of this type cannot be used as base sorted instances RSet::::new() } - -// // this is OK because we just dont generate an index for `soup` -// #[flux::sig(fn(soup:RSet))] -// pub fn test04(_s: RSet) {} - -#[flux::sig(fn(RSet[@salt]))] //~ ERROR type cannot be refined -pub fn test05(s: RSet) -where - T: Eq + Hash, -{ -} diff --git a/crates/flux-tests/tests/neg/error_messages/wf/kinds01.rs b/crates/flux-tests/tests/neg/error_messages/wf/kinds01.rs index 851acccdae..a4cb743b1c 100644 --- a/crates/flux-tests/tests/neg/error_messages/wf/kinds01.rs +++ b/crates/flux-tests/tests/neg/error_messages/wf/kinds01.rs @@ -5,32 +5,13 @@ use std::hash::Hash; use rset::RSet; -fn mk_eq_hash() -> impl Eq + Hash { - 0 -} - -#[flux::sig(fn(x:T) -> T[x])] -fn id(x: T) {} - -pub fn test_base() { - let z = mk_eq_hash(); // TODO: REJECT - id(z); -} - -fn bob(x: T) { - id(x) // TODO: REJECT-but-actually-ok -} - -fn test_bob(x: T) { - let z = mk_eq_hash(); - bob(z) // TODO: REJECT-but-actually-ok -} - -/// TODO: This currently crashes. We should gracefully reject it. -/// x: impl Eq + Hash -/// This will try to create an `RSet` which can't be put into RSet -fn test02() { - let x = mk_eq_hash(); - let mut s = RSet::new(); - s.insert(x); +// this is OK because we just dont generate an index for `soup` +#[flux::sig(fn(soup:RSet))] +pub fn test04(_s: RSet) {} + +#[flux::sig(fn(RSet[@salt]))] //~ ERROR type cannot be refined +pub fn test05(_s: RSet) +where + T: Eq + Hash, +{ } diff --git a/crates/flux-tests/tests/neg/error_messages/wf/kinds02.rs b/crates/flux-tests/tests/neg/error_messages/wf/kinds02.rs new file mode 100644 index 0000000000..3ecc680ff6 --- /dev/null +++ b/crates/flux-tests/tests/neg/error_messages/wf/kinds02.rs @@ -0,0 +1,38 @@ +#[path = "../../../lib/rset.rs"] +pub mod rset; + +use std::hash::Hash; + +use rset::RSet; + +fn mk_eq_hash() -> impl Eq + Hash { + 0 +} + +#[flux::sig(fn(x:T) -> T[x])] +fn id(x: T) -> T { + x +} + +// This will try to call id with an `RSet` which can't be a "base" +pub fn test00() { + let z = mk_eq_hash(); + id(z); //~ ERROR cannot instantiate +} + +// This will try to create an `RSet` which can't be put into RSet +pub fn test01() { + let x = mk_eq_hash(); + let mut s = RSet::new(); //~ ERROR cannot instantiate + s.insert(x); +} + +// #[flux::sig(fn(x:T))] +// pub fn test01(x: T) { +// id(x); // TODO: REJECT-but-actually-ok +// } + +// fn test_bob(x: T) { +// let z = mk_eq_hash(); +// bob(z); // TODO: REJECT-but-actually-ok +// } diff --git a/crates/flux-tests/tests/neg/surface/maps00.rs b/crates/flux-tests/tests/neg/surface/maps00.rs index d91e84dc83..b104432fc7 100644 --- a/crates/flux-tests/tests/neg/surface/maps00.rs +++ b/crates/flux-tests/tests/neg/surface/maps00.rs @@ -13,7 +13,6 @@ pub fn test() { m.set(k0, 1); m.set(k1, 2); - assert(*m.get(&k0).unwrap() == 1); assert(*m.get(&k1).unwrap() == 2); assert(*m.get(&k2).unwrap() == 3); //~ ERROR refinement type diff --git a/crates/flux-tests/tests/neg/surface/rset00.rs b/crates/flux-tests/tests/neg/surface/rset00.rs index 1bcfa6afdd..669cbee38a 100644 --- a/crates/flux-tests/tests/neg/surface/rset00.rs +++ b/crates/flux-tests/tests/neg/surface/rset00.rs @@ -15,7 +15,7 @@ pub fn id(s: RSet) -> RSet { fn assert(_b: bool) {} #[flux::trusted] -#[flux::sig(fn() -> RSet[set_empty(0)])] +#[flux::sig(fn() -> RSet[set_empty(0)])] pub fn empty() -> RSet { let inner = std::collections::HashSet::new(); RSet { inner } diff --git a/crates/flux-tests/tests/pos/surface/rset00.rs b/crates/flux-tests/tests/pos/surface/rset00.rs index bb9c1abd76..d85211c8a3 100644 --- a/crates/flux-tests/tests/pos/surface/rset00.rs +++ b/crates/flux-tests/tests/pos/surface/rset00.rs @@ -15,7 +15,7 @@ pub fn id(s: RSet) -> RSet { fn assert(_b: bool) {} #[flux::trusted] -#[flux::sig(fn() -> RSet[set_empty(0)])] +#[flux::sig(fn() -> RSet[set_empty(0)])] pub fn empty() -> RSet { let inner = std::collections::HashSet::new(); RSet { inner } @@ -31,7 +31,7 @@ where } #[flux::trusted] -#[flux::sig(fn(set: &RSet[@s], &A[@elem]) -> bool[set_is_in(elem, s.elems)])] +#[flux::sig(fn(set: &RSet[@soup], &A[@elem]) -> bool[set_is_in(elem, soup.elems)])] pub fn contains(set: &RSet, elem: &A) -> bool where A: Eq + Hash,