From cd7dd7f17f5c740422e162f5a251a20dc9a2131d Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Sat, 30 Dec 2023 07:39:13 -0800 Subject: [PATCH] stash: check-trait-impl --- crates/flux-fhir-analysis/src/lib.rs | 3 - crates/flux-refineck/src/checker.rs | 67 ++++++++++--------- .../pos/surface/refined_fn_in_trait_01.rs | 39 +++-------- 3 files changed, 46 insertions(+), 63 deletions(-) diff --git a/crates/flux-fhir-analysis/src/lib.rs b/crates/flux-fhir-analysis/src/lib.rs index 2a999b1feb..c0b0495dcb 100644 --- a/crates/flux-fhir-analysis/src/lib.rs +++ b/crates/flux-fhir-analysis/src/lib.rs @@ -249,9 +249,6 @@ fn variants_of( fn fn_sig(genv: &GlobalEnv, def_id: LocalDefId) -> QueryResult> { let fn_sig = genv.map().get_fn_sig(def_id); - - println!("TRACE: fn_sig FOO {def_id:?} ==> lifted = {:?}", fn_sig.lifted); - let wfckresults = genv.check_wf(def_id)?; let defns = genv.defns()?; let fn_sig = conv::conv_fn_sig(genv, def_id, fn_sig, &wfckresults)? diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 8e9aafdd71..f1341d0d5e 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -150,36 +150,39 @@ impl<'a, 'tcx> Checker<'a, 'tcx, ShapeMode> { } } -/// This function returns the trait_method corresponding to an impl_method defined by `def_id` (if such a method exists). -fn impl_trait_method(genv: &GlobalEnv, def_id: DefId) -> Option { - let impl_id = genv.tcx.impl_of_method(def_id)?; - let trait_id = genv.tcx.trait_id_of_impl(impl_id)?; - let impl_ids = genv.tcx.impl_item_implementor_ids(impl_id); - for trait_f in genv.tcx.associated_item_def_ids(trait_id) { - if impl_ids.get(trait_f) == Some(&def_id) { - return Some(*trait_f); - } - } - None -} - -fn checker_sig( - genv: &GlobalEnv, - def_id: LocalDefId, -) -> Result, CheckerError> { - let fn_sig = genv.fn_sig(def_id).with_span(genv.tcx.def_span(def_id))?; - let is_lifted = fn_sig.0.as_ref().skip_binder().lifted(); - if let Some(trait_method_id) = impl_trait_method(genv, def_id.to_def_id()) - && is_lifted - { - let method_sig = genv - .fn_sig(trait_method_id) - .with_span(genv.tcx.def_span(trait_method_id))?; - println!("TRACE: checker_sig {def_id:?} ==> {fn_sig:?} ==> {method_sig:?}"); - next_how_to_instantiate_method_sig() - } - Ok(fn_sig) -} +// DEAD/FROZEN CODE for TODO(check-trait-impl) +// /// This function returns the trait_method corresponding to an impl_method defined by `def_id` (if such a method exists). +// fn impl_trait_method(genv: &GlobalEnv, def_id: DefId) -> Option { +// let impl_id = genv.tcx.impl_of_method(def_id)?; +// let trait_ref = genv.tcx.impl_trait_ref(impl_id); +// println!("TRACE: impl_trait_method {def_id:?} ==> {trait_ref:?}"); +// let trait_id = genv.tcx.trait_id_of_impl(impl_id)?; +// let impl_ids = genv.tcx.impl_item_implementor_ids(impl_id); +// for trait_f in genv.tcx.associated_item_def_ids(trait_id) { +// if impl_ids.get(trait_f) == Some(&def_id) { +// return Some(*trait_f); +// } +// } +// None +// } + +// fn checker_sig( +// genv: &GlobalEnv, +// def_id: LocalDefId, +// ) -> Result, CheckerError> { +// let fn_sig = genv.fn_sig(def_id).with_span(genv.tcx.def_span(def_id))?; +// let is_lifted = fn_sig.0.as_ref().skip_binder().lifted(); +// if let Some(trait_method_id) = impl_trait_method(genv, def_id.to_def_id()) +// && is_lifted +// { +// let method_sig = genv +// .fn_sig(trait_method_id) +// .with_span(genv.tcx.def_span(trait_method_id))?; +// println!("TRACE: checker_sig {def_id:?} ==> {fn_sig:?} ==> {method_sig:?}"); +// // next_how_to_instantiate_method_sig() +// } +// Ok(fn_sig) +// } impl<'a, 'tcx> Checker<'a, 'tcx, RefineMode> { pub(crate) fn run_in_refine_mode( @@ -189,8 +192,8 @@ impl<'a, 'tcx> Checker<'a, 'tcx, RefineMode> { bb_env_shapes: ShapeResult, config: CheckerConfig, ) -> Result<(RefineTree, KVarStore), CheckerError> { - // let fn_sig = genv.fn_sig(def_id).with_span(genv.tcx.def_span(def_id))?; - let fn_sig = checker_sig(genv, def_id)?; + // TODO(check-trait-impl) let fn_sig = checker_sig(genv, def_id)?; + let fn_sig = genv.fn_sig(def_id).with_span(genv.tcx.def_span(def_id))?; let mut kvars = fixpoint_encoding::KVarStore::new(); let mut refine_tree = RefineTree::new(); diff --git a/crates/flux-tests/tests/pos/surface/refined_fn_in_trait_01.rs b/crates/flux-tests/tests/pos/surface/refined_fn_in_trait_01.rs index 7b508e477a..01d9b6cbd1 100644 --- a/crates/flux-tests/tests/pos/surface/refined_fn_in_trait_01.rs +++ b/crates/flux-tests/tests/pos/surface/refined_fn_in_trait_01.rs @@ -2,40 +2,23 @@ pub trait MyTrait { #[flux::sig(fn bool>(&Self{v: p(v)}) -> Self{v: p(v)})] fn foo1(&self) -> Self; - - // fn foo2(&self) -> Self; } -// #[flux::sig(fn bool> (&T{v:q(v)}) -> T{v: q(v)})] -// pub fn bar1(x: &T) -> T { -// x.foo1() -// } - -// // This "verifies" unsoundly due to the parametricity of `T`. -// #[flux::sig(fn bool> (&T{v:q(v)}) -> T{v: q(v)})] -// pub fn bar2(x: &T) -> T { -// x.foo2() // UNSOUNDLY VERIFIED: https://github.com/flux-rs/flux/issues/588 -// } - -// 1. reject impl of `foo1` rejected! +#[flux::sig(fn bool> (&T{v:q(v)}) -> T{v: q(v)})] +pub fn bar1(x: &T) -> T { + x.foo1() +} impl MyTrait for i32 { - // #[flux::sig(fn bool>(&i32{v: p(v)}) -> i32{v: p(v)})] // WORKS - // #[flux::sig(fn bool>(&Self{v: p(v)}) -> Self{v: p(v)})] fn foo1(&self) -> Self { - 12 //~ ERROR refinement type - // *self // OK + *self } - - // fn foo2(&self) -> Self { - // 12 // *self - // } } -// #[flux::sig(fn(bool[true]))] -// fn assert(_b: bool) {} +#[flux::sig(fn(bool[true]))] +fn assert(_b: bool) {} -// pub fn test() { -// let x = 42; -// assert(x.foo1() == 42); -// } +pub fn test() { + let x = 42; + assert(bar1(&x) == 42); +}