From 5810eeb13548f1273c3e1dcee4bf8b7831d4c81e Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 22 Nov 2024 16:31:23 -0800 Subject: [PATCH 1/3] beef up infer-mut-hack --- crates/flux-middle/src/rty/mod.rs | 3 +++ crates/flux-refineck/src/checker.rs | 41 +++++++++++++++++++++++------ 2 files changed, 36 insertions(+), 8 deletions(-) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index c3bf82b3ed..93f9e1b16b 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -1096,6 +1096,9 @@ impl Ty { &self.0 } + pub fn is_indexed(&self) -> bool { + matches!(self.kind(), TyKind::Indexed(..)) + } /// Dummy type used for the `Self` of a `TraitRef` created when converting a trait object, and /// which gets removed in `ExistentialTraitRef`. This type must not appear anywhere in other /// converted types and must be a valid `rustc` type (i.e., we must be able to call `to_rustc` diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index ad576482c0..d571c6fcee 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -12,10 +12,14 @@ use flux_middle::{ queries::QueryResult, query_bug, rty::{ - self, fold::TypeFoldable, refining::Refiner, AdtDef, BaseTy, Binder, Bool, Clause, - CoroutineObligPredicate, EarlyBinder, Expr, FnOutput, FnTraitPredicate, GenericArg, - GenericArgs, GenericArgsExt as _, Int, IntTy, Mutability, Path, PolyFnSig, PtrKind, Ref, - RefineArgs, RefineArgsExt, Region::ReStatic, Ty, TyKind, Uint, UintTy, VariantIdx, + self, + fold::{TypeFoldable, TypeFolder, TypeSuperFoldable}, + refining::Refiner, + AdtDef, BaseTy, Binder, Bool, Clause, CoroutineObligPredicate, EarlyBinder, Expr, FnOutput, + FnTraitPredicate, GenericArg, GenericArgs, GenericArgsExt as _, Int, IntTy, Mutability, + Path, PolyFnSig, PtrKind, Ref, RefineArgs, RefineArgsExt, + Region::ReStatic, + Ty, TyKind, Uint, UintTy, VariantIdx, }, }; use flux_rustc_bridge::{ @@ -814,9 +818,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { at.fun_arg_subtyping(env, &actual, formal, ConstrReason::Call) .with_span(span)?; } - // Replace evars - let evars_sol = infcx.pop_scope().unwrap(); + let evars_sol = infcx.pop_scope().unwrap(); // with_span(span)?; env.replace_evars(&evars_sol); infcx.replace_evars(&evars_sol); @@ -1705,6 +1708,29 @@ fn all_predicates_of( .flatten() } +struct SkipConstr; + +impl TypeFolder for SkipConstr { + fn fold_ty(&mut self, ty: &rty::Ty) -> rty::Ty { + if let rty::TyKind::Constr(_, inner_ty) = ty.kind() { + inner_ty.fold_with(self) + } else { + ty.super_fold_with(self) + } + } +} + +fn is_indexed_mut_skipping_constr(ty: &Ty) -> bool { + let ty = SkipConstr.fold_ty(ty); + if let rty::Ref!(_, inner_ty, Mutability::Mut) = ty.kind() + && let TyKind::Indexed(..) = inner_ty.kind() + { + true + } else { + false + } +} + /// HACK(nilehmann) This let us infer parameters under mutable references for the simple case /// where the formal argument is of the form `&mut B[@n]`, e.g., the type of the first argument /// to `RVec::get_mut` is `&mut RVec[@n]`. We should remove this after we implement opening of @@ -1725,8 +1751,7 @@ fn infer_under_mut_ref_hack( ) .map(|(actual, formal)| { if let rty::Ref!(.., Mutability::Mut) = actual.kind() - && let rty::Ref!(_, ty, Mutability::Mut) = formal.kind() - && let TyKind::Indexed(..) = ty.kind() + && is_indexed_mut_skipping_constr(formal) { rcx.hoister(AssumeInvariants::No) .hoist_inside_mut_refs(true) From 593542136484e281a8509cffd80fcf6e80314240 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 22 Nov 2024 16:59:49 -0800 Subject: [PATCH 2/3] beef up infer-mut-hack --- crates/flux-refineck/src/checker.rs | 4 +--- tests/tests/neg/surface/mut_hack00.rs | 15 +++++++++++++++ tests/tests/pos/surface/mut_hack00.rs | 16 ++++++++++++++++ 3 files changed, 32 insertions(+), 3 deletions(-) create mode 100644 tests/tests/neg/surface/mut_hack00.rs create mode 100644 tests/tests/pos/surface/mut_hack00.rs diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index d18f7876bd..66eed5ed0a 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -818,7 +818,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { .with_span(span)?; } // Replace evars - let evars_sol = infcx.pop_scope().unwrap(); // with_span(span)?; + let evars_sol = infcx.pop_scope().with_span(span)?; env.replace_evars(&evars_sol); infcx.replace_evars(&evars_sol); @@ -1743,8 +1743,6 @@ fn infer_under_mut_ref_hack( .map(|(actual, formal)| { if let rty::Ref!(.., Mutability::Mut) = actual.kind() && is_indexed_mut_skipping_constr(formal) - // && let rty::Ref!(_, ty, Mutability::Mut) = formal.kind() - // && let TyKind::Indexed(..) = ty.kind() { rcx.hoister(AssumeInvariants::No) .hoist_inside_mut_refs(true) diff --git a/tests/tests/neg/surface/mut_hack00.rs b/tests/tests/neg/surface/mut_hack00.rs new file mode 100644 index 0000000000..b69d1e229f --- /dev/null +++ b/tests/tests/neg/surface/mut_hack00.rs @@ -0,0 +1,15 @@ +#[flux::sig(fn (xs: &mut { [i32][@n] | n > 1}))] +fn lib1(_xs: &mut [i32]) {} + +#[flux::sig(fn (xs: { &mut [i32][@n] | n > 1}))] +fn lib2(_xs: &mut [i32]) {} + +fn boo() -> &'static mut [i32] { + todo!() +} + +fn test() { + let ys = boo(); + lib1(ys); //~ ERROR: refinement type + lib2(ys); //~ ERROR: refinement type +} diff --git a/tests/tests/pos/surface/mut_hack00.rs b/tests/tests/pos/surface/mut_hack00.rs new file mode 100644 index 0000000000..9552abcf66 --- /dev/null +++ b/tests/tests/pos/surface/mut_hack00.rs @@ -0,0 +1,16 @@ +#[flux::sig(fn (xs: &mut { [i32][@n] | n > 1}))] +fn lib1(_xs: &mut [i32]) {} + +#[flux::sig(fn (xs: {&mut [i32][@n] | n > 1}))] +fn lib2(_xs: &mut [i32]) {} + +#[flux::sig(fn () -> &mut [i32][10])] +fn boo() -> &'static mut [i32] { + todo!() +} + +fn test() { + let ys = boo(); + lib2(ys); + lib1(ys); +} From dbc7284be76db400800508655ecf56e36eae6031 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 22 Nov 2024 17:00:21 -0800 Subject: [PATCH 3/3] beef up infer-mut-hack --- crates/flux-middle/src/rty/mod.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 93f9e1b16b..c3bf82b3ed 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -1096,9 +1096,6 @@ impl Ty { &self.0 } - pub fn is_indexed(&self) -> bool { - matches!(self.kind(), TyKind::Indexed(..)) - } /// Dummy type used for the `Self` of a `TraitRef` created when converting a trait object, and /// which gets removed in `ExistentialTraitRef`. This type must not appear anywhere in other /// converted types and must be a valid `rustc` type (i.e., we must be able to call `to_rustc`