Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Beef up infer-mut-hack #904

Merged
merged 4 commits into from
Nov 23, 2024
Merged

Beef up infer-mut-hack #904

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
5810eeb
beef up infer-mut-hack
ranjitjhala Nov 23, 2024
4ccf53c
beef up infer-mut-hack
ranjitjhala Nov 23, 2024
5935421
beef up infer-mut-hack
ranjitjhala Nov 23, 2024
dbc7284
beef up infer-mut-hack
ranjitjhala Nov 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 33 additions & 8 deletions crates/flux-refineck/src/checker.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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::{
Expand Down Expand Up @@ -813,9 +817,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().with_span(span)?;
env.replace_evars(&evars_sol);
infcx.replace_evars(&evars_sol);

Expand Down Expand Up @@ -1704,6 +1707,29 @@ fn all_predicates_of(
.flatten()
}

struct SkipConstr;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ranjitjhala

We already have Ty::unconstr which is a more general version of this.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Interesting -- didn't know about it!

But, not really, replacing

let ty = SkipConstr.fold_ty(ty);

with

 let (ty, _) = ty.unconstr();

Doesn't seem to work -- looks like unconstr is not "deep": it expects the Constr at the very top?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like unconstr just peels away all the "topmost" Constr -- the moment it hits something else it stops.

So it won't work with

#[flux::sig(fn (xs: &mut { [i32][@n] | n > 1}))]
fn lib1(_xs: &mut [i32]) {}

Copy link
Member

@nilehmann nilehmann Nov 23, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You first need to match on the &mut T and then unconstr the T

 if let rty::Ref!(_, deref_ty, Mutability::Mut) = ty.kind()
    && let (deref_ty, _) = deref_ty.unconstr()
    && let TyKind::Indexed(..) = inner_ty.kind()

I wonder though if there's a clean way to handle this during canonicalization (the thing unpack is implementing on top of). It is always safe to turn an &mut {T | p} into {&mut T | p} so we could get rid of it during unpack

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is why I have two tests -- the other one flips the order which fails your method

#[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]) {}

But yes, if you had canonicalized presumably lib1 gets turned into lib2?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ah yeah, you'd need to unconstr twice

let (ty, _) = ty.unconstr();
if let rty::Ref!(_, deref_ty, Mutability::Mut) = ty.kind() 
    && let (deref_ty, _) = deref_ty.unconstr() 
    && let TyKind::Indexed(..) = inner_ty.kind()

I still think there has to be a nice way in which we can canonicalize types before pattern matching on them. The canonicalize infra is almost there...


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<T>[@n]`. We should remove this after we implement opening of
Expand All @@ -1716,8 +1742,7 @@ fn infer_under_mut_ref_hack(
iter::zip(actuals, fn_sig.skip_binder_ref().skip_binder_ref().inputs())
.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)
Expand Down
15 changes: 15 additions & 0 deletions tests/tests/neg/surface/mut_hack00.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
}
16 changes: 16 additions & 0 deletions tests/tests/pos/surface/mut_hack00.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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);
}
Loading