stash: check-trait-impl

flux-rs · Dec 30, 2023 · cd7dd7f · cd7dd7f
1 parent c0e1f88
commit cd7dd7f
Show file tree

Hide file tree

Showing 3 changed files with 46 additions and 63 deletions.
diff --git 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<rty::EarlyBinder<rty::PolyFnSig>> {
     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
@@ -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<DefId> {
-    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<EarlyBinder<PolyFnSig>, 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<DefId> {
+//     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<EarlyBinder<PolyFnSig>, 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
@@ -2,40 +2,23 @@
 pub trait MyTrait {
     #[flux::sig(fn<refine p: Self -> bool>(&Self{v: p(v)}) -> Self{v: p(v)})]
     fn foo1(&self) -> Self;
-
-    // fn foo2(&self) -> Self;
 }
 
-// #[flux::sig(fn<T as base, refine q: T -> bool> (&T{v:q(v)}) -> T{v: q(v)})]
-// pub fn bar1<T: MyTrait>(x: &T) -> T {
-//     x.foo1()
-// }
-
-// // This "verifies" unsoundly due to the parametricity of `T`.
-// #[flux::sig(fn<T as base, refine q: T -> bool> (&T{v:q(v)}) -> T{v: q(v)})]
-// pub fn bar2<T: MyTrait>(x: &T) -> T {
-//     x.foo2() // UNSOUNDLY VERIFIED: https://github.com/flux-rs/flux/issues/588
-// }
-
-// 1. reject impl of `foo1` rejected!
+#[flux::sig(fn<T as base, refine q: T -> bool> (&T{v:q(v)}) -> T{v: q(v)})]
+pub fn bar1<T: MyTrait>(x: &T) -> T {
+    x.foo1()
+}
 
 impl MyTrait for i32 {
-    // #[flux::sig(fn<refine p: int -> bool>(&i32{v: p(v)}) -> i32{v: p(v)})]      // WORKS
-    // #[flux::sig(fn<refine p: Self -> 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);
+}