From 7085a0d8885a7514a8ee478093fd9c93e348006b Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Wed, 4 Sep 2024 10:26:53 -0700 Subject: [PATCH 1/4] blerp --- crates/flux-fhir-analysis/src/conv/struct_compat.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/struct_compat.rs b/crates/flux-fhir-analysis/src/conv/struct_compat.rs index 9d2deabb6b..408fb1fc01 100644 --- a/crates/flux-fhir-analysis/src/conv/struct_compat.rs +++ b/crates/flux-fhir-analysis/src/conv/struct_compat.rs @@ -266,6 +266,7 @@ impl<'genv, 'tcx> Zipper<'genv, 'tcx> { assert_eq_or_incompatible(pty_a, pty_b) } (rty::TyKind::Alias(kind_a, aty_a), rty::TyKind::Alias(kind_b, aty_b)) => { + println!("TRACE: zip_ty ALIAS ({aty_a:?}, {aty_b:?})"); assert_eq_or_incompatible(kind_a, kind_b)?; assert_eq_or_incompatible(aty_a.def_id, aty_b.def_id)?; assert_eq_or_incompatible(aty_a.args.len(), aty_b.args.len())?; @@ -289,7 +290,8 @@ impl<'genv, 'tcx> Zipper<'genv, 'tcx> { } fn zip_bty(&mut self, a: &rty::BaseTy, b: &rty::BaseTy) -> Result<(), Error> { - match (a, b) { + println!("TRACE: zip_bty({:?}, {:?})", a, b); + let res = match (a, b) { (rty::BaseTy::Int(ity_a), rty::BaseTy::Int(ity_b)) => { assert_eq_or_incompatible(ity_a, ity_b) } @@ -347,7 +349,9 @@ impl<'genv, 'tcx> Zipper<'genv, 'tcx> { bug!("unexpected type `{a:?}`"); } _ => Err(Error::Incompatible), - } + }; + println!("TRACE: zip_bty({:?}, {:?}) ", a, b); + res } fn zip_generic_arg(&mut self, a: &rty::GenericArg, b: &rty::GenericArg) -> Result<(), Error> { From 8b51db4da64e8b606b51bbfac6e9862fc6fadf5f Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 5 Sep 2024 11:35:52 -0700 Subject: [PATCH 2/4] temp checkin --- crates/flux-fhir-analysis/src/conv/struct_compat.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/struct_compat.rs b/crates/flux-fhir-analysis/src/conv/struct_compat.rs index 74773333e6..fb9584dbbd 100644 --- a/crates/flux-fhir-analysis/src/conv/struct_compat.rs +++ b/crates/flux-fhir-analysis/src/conv/struct_compat.rs @@ -285,7 +285,7 @@ impl<'genv, 'tcx> Zipper<'genv, 'tcx> { } fn zip_bty(&mut self, a: &rty::BaseTy, b: &rty::BaseTy) -> Result<(), Error> { - let res = match (a, b) { + match (a, b) { (rty::BaseTy::Int(ity_a), rty::BaseTy::Int(ity_b)) => { assert_eq_or_incompatible(ity_a, ity_b) } @@ -343,8 +343,7 @@ impl<'genv, 'tcx> Zipper<'genv, 'tcx> { bug!("unexpected type `{a:?}`"); } _ => Err(Error::Incompatible), - }; - res + } } fn zip_generic_arg(&mut self, a: &rty::GenericArg, b: &rty::GenericArg) -> Result<(), Error> { From f07a220b22af6bc70e4d7fdbed1c0cf0ded0d95c Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 10 Sep 2024 18:49:41 -0700 Subject: [PATCH 3/4] temp checkin --- crates/flux-middle/src/rty/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 72d0db7d0d..6c910c367b 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -1321,7 +1321,7 @@ impl TyS { if let TyKind::Indexed(BaseTy::Adt(adt_def, args), idx) = self.kind() { (adt_def, args, idx) } else { - bug!("expected adt") + bug!("expected an adt") } } From 0346d5014c8af1b81f733de18048e5902937b35e Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 17 Sep 2024 09:49:38 -0700 Subject: [PATCH 4/4] add fnptr test --- crates/flux-infer/src/infer.rs | 4 ++++ tests/tests/pos/surface/fnptr00.rs | 18 ++++++++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 tests/tests/pos/surface/fnptr00.rs diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs index 0b8026a16f..ffd5258c82 100644 --- a/crates/flux-infer/src/infer.rs +++ b/crates/flux-infer/src/infer.rs @@ -550,6 +550,10 @@ impl Sub { } Ok(()) } + (BaseTy::FnPtr(sig_a), BaseTy::FnPtr(sig_b)) => { + assert_eq!(sig_a, sig_b); + Ok(()) + } _ => Err(query_bug!("incompatible base types: `{a:?}` - `{b:?}`"))?, } } diff --git a/tests/tests/pos/surface/fnptr00.rs b/tests/tests/pos/surface/fnptr00.rs new file mode 100644 index 0000000000..5abf3d3dca --- /dev/null +++ b/tests/tests/pos/surface/fnptr00.rs @@ -0,0 +1,18 @@ +#![allow(unused)] + +type Binop = fn(i32, i32) -> i32; + +struct Foo { + f: Binop, +} + +// TODO: should actually support the below, not just leave it as `trusted` +#[flux::trusted] +fn bar(b: Binop) -> i32 { + b(3, 4) +} + +fn test00(foo: Foo) -> i32 { + let x = bar(foo.f); + x +}