From cf3d30e05fc8820fe999f703d7df948e5604a90f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 31 Jan 2025 16:19:41 +0100 Subject: [PATCH 1/8] drive-by: add test --- .../assoc-ty-via-supertrait-and-bounds.out | 19 ++ .../assoc-ty-via-supertrait-and-bounds.rs | 22 ++ .../ui/type_inference_is_order_dependent.out | 188 ++++++++++++++++++ .../ui/type_inference_is_order_dependent.rs | 32 +++ 4 files changed, 261 insertions(+) create mode 100644 charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out create mode 100644 charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs create mode 100644 charon/tests/ui/type_inference_is_order_dependent.out create mode 100644 charon/tests/ui/type_inference_is_order_dependent.rs diff --git a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out new file mode 100644 index 00000000..041c7ecb --- /dev/null +++ b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out @@ -0,0 +1,19 @@ +error: Could not compute the value of Clause1_1::Clause0::Output needed to update generics <()> for item test_crate::HasOutput. + Constraints in scope: + + --> tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs:21:5 + | +21 | take::>() + | ^^^^^^^^^^^^^^^^^^^^^ + | + +error: Could not compute the value of Clause1_1::Clause0::Output needed to update generics <()> for item test_crate::HasOutput. + Constraints in scope: + + --> tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs:21:5 + | +21 | take::>() + | ^^^^^^^^^^^^^^^^^^^^^ + | + +ERROR The extraction generated 2 errors diff --git a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs new file mode 100644 index 00000000..2ffbe34b --- /dev/null +++ b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs @@ -0,0 +1,22 @@ +//@ known-failure +//@ charon-args=--remove-associated-types=* +pub trait HasOutput { + type Output; +} +impl HasOutput for () { + type Output = (); +} + +pub trait HasOutput2: HasOutput {} +impl HasOutput2 for () {} + +struct Wrapper(T); +impl HasOutput for Wrapper { + type Output = ::Output; +} +impl HasOutput2 for Wrapper {} + +fn take() {} +fn main() { + take::>() +} diff --git a/charon/tests/ui/type_inference_is_order_dependent.out b/charon/tests/ui/type_inference_is_order_dependent.out new file mode 100644 index 00000000..5019a857 --- /dev/null +++ b/charon/tests/ui/type_inference_is_order_dependent.out @@ -0,0 +1,188 @@ +# Final LLBC before serialization: + +trait core::marker::Sized + +trait test_crate::Left +{ + parent_clause0 : [@TraitClause0]: core::marker::Sized +} + +trait test_crate::Right +{ + parent_clause0 : [@TraitClause0]: core::marker::Sized +} + +trait test_crate::Join +{ + parent_clause0 : [@TraitClause0]: core::marker::Sized + fn test = test_crate::Join::test +} + +trait core::default::Default +{ + parent_clause0 : [@TraitClause0]: core::marker::Sized + fn default = core::default::Default::default +} + +opaque type core::fmt::Formatter<'a> + where + 'a : 'a, + +enum core::result::Result + where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + = +| Ok(T) +| Err(E) + + +struct core::fmt::Error = {} + +trait core::fmt::Debug +{ + fn fmt<'_0, '_1, '_2> = core::fmt::Debug::fmt<'_0_0, '_0_1, '_0_2, Self> +} + +opaque type core::fmt::Arguments<'a> + where + 'a : 'a, + +opaque type core::fmt::rt::Argument<'a> + +fn core::default::Default::default() -> Self + +fn core::fmt::rt::{core::fmt::rt::Argument<'_0>}#1::new_debug<'_0, '_1, T>(@1: &'_1 (T)) -> core::fmt::rt::Argument<'_1> +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::fmt::Debug, + +fn core::fmt::{core::fmt::Arguments<'a>}#2::new_v1<'a, const P : usize, const A : usize>(@1: &'a (Array<&'static (Str), const P : usize>), @2: &'a (Array, const A : usize>)) -> core::fmt::Arguments<'a> + +fn std::io::stdio::_print<'_0>(@1: core::fmt::Arguments<'_0>) + +fn test_crate::{impl test_crate::Join for T}::test() +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: test_crate::Left, + [@TraitClause3]: test_crate::Right, + [@TraitClause4]: core::default::Default, + [@TraitClause5]: core::fmt::Debug, +{ + let @0: (); // return + let @1: (); // anonymous local + let @2: core::fmt::Arguments<'_>; // anonymous local + let @3: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local + let @4: &'_ (Array<&'_ (Str), 2 : usize>); // anonymous local + let @5: Array<&'_ (Str), 2 : usize>; // anonymous local + let @6: &'_ (Array, 1 : usize>); // anonymous local + let @7: &'_ (Array, 1 : usize>); // anonymous local + let @8: Array, 1 : usize>; // anonymous local + let @9: core::fmt::rt::Argument<'_>; // anonymous local + let @10: &'_ (U); // anonymous local + let @11: &'_ (U); // anonymous local + let @12: U; // anonymous local + let @13: (); // anonymous local + + @5 := [const (""), const (" +"); 2 : usize] + @4 := &@5 + @3 := &*(@4) + @12 := @TraitClause4::default() + @11 := &@12 + @10 := &*(@11) + @9 := core::fmt::rt::{core::fmt::rt::Argument<'_0>}#1::new_debug<'_, '_, U>[@TraitClause1, @TraitClause5](move (@10)) + drop @10 + @8 := [move (@9); 1 : usize] + drop @9 + @7 := &@8 + @6 := &*(@7) + @2 := core::fmt::{core::fmt::Arguments<'a>}#2::new_v1<'_, 2 : usize, 1 : usize>(move (@3), move (@6)) + drop @6 + drop @3 + @1 := std::io::stdio::_print<'_>(move (@2)) + drop @2 + drop @12 + drop @12 + drop @11 + drop @8 + drop @7 + drop @5 + drop @4 + drop @1 + @13 := () + @0 := move (@13) + @0 := () + return +} + +impl test_crate::{impl test_crate::Join for T} : test_crate::Join +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: test_crate::Left, + [@TraitClause3]: test_crate::Right, + [@TraitClause4]: core::default::Default, + [@TraitClause5]: core::fmt::Debug, +{ + parent_clause0 = @TraitClause1 + fn test = test_crate::{impl test_crate::Join for T}::test[@TraitClause0, @TraitClause1, @TraitClause2, @TraitClause3, @TraitClause4, @TraitClause5] +} + +impl test_crate::{impl test_crate::Left for T}#1 : test_crate::Left +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: core::default::Default, + [@TraitClause3]: core::fmt::Debug, +{ + parent_clause0 = @TraitClause1 +} + +impl test_crate::{impl test_crate::Right for T}#2 : test_crate::Right +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: core::default::Default, + [@TraitClause3]: core::fmt::Debug, +{ + parent_clause0 = @TraitClause1 +} + +fn core::default::{impl core::default::Default for bool}#1::default() -> bool + +impl core::default::{impl core::default::Default for bool}#1 : core::default::Default +{ + parent_clause0 = core::marker::Sized + fn default = core::default::{impl core::default::Default for bool}#1::default +} + +fn core::fmt::{impl core::fmt::Debug for bool}#14::fmt<'_0, '_1, '_2>(@1: &'_0 (bool), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>[core::marker::Sized<()>, core::marker::Sized] + +impl core::fmt::{impl core::fmt::Debug for bool}#14 : core::fmt::Debug +{ + fn fmt<'_0, '_1, '_2> = core::fmt::{impl core::fmt::Debug for bool}#14::fmt<'_0_0, '_0_1, '_0_2> +} + +fn test_crate::try_it() +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::default::Default, + [@TraitClause2]: core::fmt::Debug, + [@TraitClause3]: test_crate::Left, + [@TraitClause4]: test_crate::Right, +{ + let @0: (); // return + + @0 := test_crate::{impl test_crate::Join for T}::test[@TraitClause0, core::marker::Sized, @TraitClause3, test_crate::{impl test_crate::Right for T}#2[@TraitClause0, core::marker::Sized, core::default::{impl core::default::Default for bool}#1, core::fmt::{impl core::fmt::Debug for bool}#14], core::default::{impl core::default::Default for bool}#1, core::fmt::{impl core::fmt::Debug for bool}#14]() + @0 := () + return +} + +fn test_crate::Join::test() + +fn core::fmt::Debug::fmt<'_0, '_1, '_2, Self>(@1: &'_0 (Self), @2: &'_1 mut (core::fmt::Formatter<'_2>)) -> core::result::Result<(), core::fmt::Error>[core::marker::Sized<()>, core::marker::Sized] + + + diff --git a/charon/tests/ui/type_inference_is_order_dependent.rs b/charon/tests/ui/type_inference_is_order_dependent.rs new file mode 100644 index 00000000..ee917ae9 --- /dev/null +++ b/charon/tests/ui/type_inference_is_order_dependent.rs @@ -0,0 +1,32 @@ +//! See https://github.com/rust-lang/rust/issues/41756. +use std::fmt::Debug; + +trait Left {} +trait Right {} + +trait Join { + fn test(); +} + +// If we swap the two clauses, a different type is selected in `try_it`. +impl Join for T +where + T: Left, + T: Right, + U: Default + Debug, +{ + fn test() { + println!("{:?}", U::default()) + } +} + +impl Left for T {} +impl Right for T {} + +fn try_it() +where + T: Left, + T: Right<()>, +{ + >::test() +} From 72b8890395ceff69cbffe6836a5ba3faaacd37f1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 10 Feb 2025 17:07:14 +0100 Subject: [PATCH 2/8] drive-by: correctly pass rustc args in the `--no-cargo` case --- charon/src/bin/charon/main.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/charon/src/bin/charon/main.rs b/charon/src/bin/charon/main.rs index ca348290..e2bc0af2 100644 --- a/charon/src/bin/charon/main.rs +++ b/charon/src/bin/charon/main.rs @@ -187,6 +187,10 @@ pub fn main() -> anyhow::Result<()> { // Run just the driver. let mut cmd = driver_cmd()?; + for arg in std::mem::take(&mut options.rustc_args) { + cmd.arg(arg); + } + cmd.env(CHARON_ARGS, serde_json::to_string(&options).unwrap()); // Make sure the build target is explicitly set. This is needed to detect which crates are From 1d345321317710c2f9254d1f28064878e2ed52c7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2025 11:55:26 +0100 Subject: [PATCH 3/8] Improve error message --- .../src/transform/expand_associated_types.rs | 28 ++++++++++++++----- .../ui/simple/assoc-type-with-fn-bound.out | 2 +- 2 files changed, 22 insertions(+), 8 deletions(-) diff --git a/charon/src/transform/expand_associated_types.rs b/charon/src/transform/expand_associated_types.rs index 19978d56..c8e4f08d 100644 --- a/charon/src/transform/expand_associated_types.rs +++ b/charon/src/transform/expand_associated_types.rs @@ -80,7 +80,7 @@ use std::{ use macros::EnumAsGetters; -use crate::{ast::*, formatter::FmtCtx, ids::Vector, pretty::FmtWithCtx, register_error}; +use crate::{ast::*, formatter::IntoFormatter, ids::Vector, pretty::FmtWithCtx, register_error}; use super::{ctx::TransformPass, TransformCtx}; @@ -983,20 +983,34 @@ impl UpdateItemBody<'_> { if let Some(tref) = base_tref.to_path() { path = path.on_tref(&tref); } + let fmt_ctx = &self.ctx.into_fmt(); + let item_name = match &args.target { + GenericsSource::Item(id) => self + .ctx + .translated + .item_name(*id) + .unwrap() + .fmt_with_ctx(fmt_ctx), + GenericsSource::Method(trait_id, method_name) => format!( + "{}::{method_name}", + self.ctx + .translated + .item_name(*trait_id) + .unwrap() + .fmt_with_ctx(fmt_ctx), + ), + GenericsSource::Builtin => format!(""), + }; register_error!( self.ctx, self.span, "Could not compute the value of {path} needed to update \ - generics {args:?} for item {:?}.\ + generics {args:?} for item {item_name}.\ \nConstraints in scope:\n{}", - args.target, self.type_replacements .iter() .flat_map(|x| x.iter()) - .map(|(path, ty)| format!( - " - {path} = {}", - ty.fmt_with_ctx(&FmtCtx::new()) - )) + .map(|(path, ty)| format!(" - {path} = {}", ty.fmt_with_ctx(fmt_ctx))) .join("\n"), ); } diff --git a/charon/tests/ui/simple/assoc-type-with-fn-bound.out b/charon/tests/ui/simple/assoc-type-with-fn-bound.out index 8a385edc..8f2b8d1d 100644 --- a/charon/tests/ui/simple/assoc-type-with-fn-bound.out +++ b/charon/tests/ui/simple/assoc-type-with-fn-bound.out @@ -1,4 +1,4 @@ -error: Could not compute the value of Self::Clause1::Clause0::Clause0::Output needed to update generics for item Item(TraitDecl(3)). +error: Could not compute the value of Self::Clause1::Clause0::Clause0::Output needed to update generics for item core::ops::function::FnOnce. Constraints in scope: - Self::Foo = @Type0_1 --> tests/ui/simple/assoc-type-with-fn-bound.rs:9:5 From 96e08cf377772474e6382839e673d345bcc57e95 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2025 18:31:30 +0100 Subject: [PATCH 4/8] Use `BindingStack` in `FmtCtx` --- charon/src/ast/types/vars.rs | 13 +- .../charon-driver/translate/translate_ctx.rs | 6 +- charon/src/pretty/formatter.rs | 111 ++++++++---------- 3 files changed, 60 insertions(+), 70 deletions(-) diff --git a/charon/src/ast/types/vars.rs b/charon/src/ast/types/vars.rs index bb645168..4a05f206 100644 --- a/charon/src/ast/types/vars.rs +++ b/charon/src/ast/types/vars.rs @@ -291,14 +291,14 @@ impl BindingStack { self.stack.pop() } /// Helper that computes the real index into `self.stack`. - fn real_index(&self, id: DeBruijnId) -> usize { - self.stack.len() - 1 - id.index + fn real_index(&self, id: DeBruijnId) -> Option { + (self.stack.len() - 1).checked_sub(id.index) } pub fn get(&self, id: DeBruijnId) -> Option<&T> { - self.stack.get(self.real_index(id)) + self.stack.get(self.real_index(id)?) } pub fn get_mut(&mut self, id: DeBruijnId) -> Option<&mut T> { - let index = self.real_index(id); + let index = self.real_index(id)?; self.stack.get_mut(index) } /// Iterate over the binding levels, from the innermost (0) out. @@ -313,6 +313,11 @@ impl BindingStack { .enumerate() .map(|(i, x)| (DeBruijnId::new(i), x)) } + pub fn map_ref<'a, U>(&'a self, f: impl FnMut(&'a T) -> U) -> BindingStack { + BindingStack { + stack: self.stack.iter().map(f).collect(), + } + } pub fn innermost(&self) -> &T { self.stack.last().unwrap() diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 22c01496..565be156 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -1370,11 +1370,7 @@ impl<'tcx, 'ctx, 'a> IntoFormatter for &'a BodyTransCtx<'tcx, 'ctx> { fn into_fmt(self) -> Self::C { FmtCtx { translated: Some(&self.t_ctx.translated), - generics: self - .binding_levels - .iter() - .map(|bl| Cow::Borrowed(&bl.params)) - .collect(), + generics: self.binding_levels.map_ref(|bl| Cow::Borrowed(&bl.params)), locals: Some(&self.locals), } } diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index a707b5be..a14163c7 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -1,5 +1,5 @@ use std::borrow::Cow; -use std::collections::VecDeque; +use std::fmt::Display; use crate::ast::*; use crate::common::TAB_INCR; @@ -80,7 +80,7 @@ impl<'a, 'b> SetGenerics<'a> for FmtCtx<'b> { fn set_generics(&'a self, generics: &'a GenericParams) -> Self::C { FmtCtx { translated: self.translated.as_deref(), - generics: [Cow::Borrowed(generics)].into(), + generics: BindingStack::new(Cow::Borrowed(generics)), locals: self.locals.as_deref(), } } @@ -125,7 +125,7 @@ impl<'a, 'b> PushBinder<'a> for FmtCtx<'b> { fn push_binder(&'a self, new_params: Cow<'a, GenericParams>) -> Self::C { let mut generics = self.generics.clone(); - generics.push_front(new_params); + generics.push(new_params); FmtCtx { translated: self.translated.as_deref(), generics, @@ -170,7 +170,7 @@ pub struct FmtCtx<'a> { pub translated: Option<&'a TranslatedCrate>, /// Generics form a stack, where each binder introduces a new level. For DeBruijn indices to /// work, we keep the innermost parameters at the start of the vector. - pub generics: VecDeque>, + pub generics: BindingStack>, pub locals: Option<&'a Locals>, } @@ -254,30 +254,48 @@ impl<'a> Formatter for FmtCtx<'a> { } } -impl<'a> Formatter for FmtCtx<'a> { - fn format_object(&self, var: RegionDbVar) -> String { +impl<'a> FmtCtx<'a> { + fn format_bound_var( + &self, + var: DeBruijnVar, + var_prefix: &str, + get: impl Fn(&GenericParams, Id) -> Result, ()>, + ) -> String { if self.generics.is_empty() { - return format!("'_{var}"); + return format!("{var_prefix}{var}"); } let (dbid, varid) = match var { - DeBruijnVar::Bound(dbid, varid) => (dbid.index, varid), - DeBruijnVar::Free(varid) => (self.generics.len() - 1, varid), + DeBruijnVar::Bound(dbid, varid) => (dbid, varid), + DeBruijnVar::Free(varid) => (self.generics.depth(), varid), }; match self .generics .get(dbid) - .and_then(|generics| generics.regions.get(varid)) + .ok_or(()) + .and_then(|generics| get(generics, varid)) { - None => format!("wrong_region('_{var})"), - Some(v) => match &v.name { - Some(name) => name.to_string(), - None if dbid == self.generics.len() - 1 => format!("'_{varid}"), - None => format!("'_{var}"), + Err(()) => format!("missing({var_prefix}{var})"), + Ok(v) => match v { + Some(name) => name, + None if dbid == self.generics.depth() => format!("{var_prefix}{varid}"), + None => format!("{var_prefix}{var}"), }, } } } +impl<'a> Formatter for FmtCtx<'a> { + fn format_object(&self, var: RegionDbVar) -> String { + self.format_bound_var(var, "'_", |generics, varid| { + generics + .regions + .get(varid) + .ok_or(()) + .map(|v| v.name.as_ref().map(|name| name.to_string())) + }) + } +} + impl<'a> Formatter<&RegionVar> for FmtCtx<'a> { fn format_object(&self, var: &RegionVar) -> String { match &var.name { @@ -289,62 +307,33 @@ impl<'a> Formatter<&RegionVar> for FmtCtx<'a> { impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, var: TypeDbVar) -> String { - if self.generics.is_empty() { - return format!("@Type{var}"); - } - let (dbid, varid) = match var { - DeBruijnVar::Bound(dbid, varid) => (dbid.index, varid), - DeBruijnVar::Free(varid) => (self.generics.len() - 1, varid), - }; - match self - .generics - .get(dbid) - .and_then(|generics| generics.types.get(varid)) - { - None => format!("missing_type_var({var})"), - Some(v) => v.to_string(), - } + self.format_bound_var(var, "@Type", |generics, varid| { + generics + .types + .get(varid) + .ok_or(()) + .map(|v| Some(v.to_string())) + }) } } impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, var: ConstGenericDbVar) -> String { - if self.generics.is_empty() { - return format!("@ConstGeneric{var}"); - } - let (dbid, varid) = match var { - DeBruijnVar::Bound(dbid, varid) => (dbid.index, varid), - DeBruijnVar::Free(varid) => (self.generics.len() - 1, varid), - }; - match self - .generics - .get(dbid) - .and_then(|generics| generics.const_generics.get(varid)) - { - None => format!("missing_cg_var({var})"), - Some(v) => v.fmt_with_ctx(self), - } + self.format_bound_var(var, "@ConstGeneric", |generics, varid| { + generics + .const_generics + .get(varid) + .ok_or(()) + .map(|v| Some(v.fmt_with_ctx(self))) + }) } } impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, var: ClauseDbVar) -> String { - if self.generics.is_empty() { - return format!("@TraitClause{var}"); - } - let (dbid, varid) = match var { - DeBruijnVar::Bound(dbid, varid) => (dbid.index, varid), - DeBruijnVar::Free(varid) => (self.generics.len() - 1, varid), - }; - match self - .generics - .get(dbid) - .and_then(|generics| generics.trait_clauses.get(varid)) - { - None => format!("missing_clause_var({var})"), - Some(_) if dbid == self.generics.len() - 1 => format!("@TraitClause{varid}"), - Some(_) => format!("@TraitClause{var}"), - } + self.format_bound_var(var, "@TraitClause", |generics, varid| { + generics.trait_clauses.get(varid).ok_or(()).map(|_| None) + }) } } From a27e183a64c79449215e64d99e164a612315cb07 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 7 Feb 2025 15:50:51 +0100 Subject: [PATCH 5/8] Abstract over getting variables from `GenericParams` --- charon/src/ast/krate.rs | 14 ++++++++ charon/src/ast/types/vars.rs | 24 +++++++++++-- charon/src/pretty/formatter.rs | 64 ++++++++++++---------------------- 3 files changed, 59 insertions(+), 43 deletions(-) diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index 835d35fa..b0fa19ab 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -3,6 +3,7 @@ use crate::formatter::{FmtCtx, Formatter, IntoFormatter}; use crate::ids::Vector; use crate::reorder_decls::DeclarationsGroups; use derive_generic_visitor::{ControlFlow, Drive, DriveMut}; +use index_vec::Idx; use indexmap::IndexSet; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; use serde::{Deserialize, Serialize}; @@ -317,6 +318,11 @@ impl<'tcx, 'ctx, 'a> IntoFormatter for &'a TranslatedCrate { } } +pub trait HasVectorOf: std::ops::Index { + fn get_vector(&self) -> &Vector; + fn get_vector_mut(&mut self) -> &mut Vector; +} + /// Delegate `Index` implementations to subfields. macro_rules! mk_index_impls { ($ty:ident.$field:ident[$idx:ty]: $output:ty) => { @@ -331,6 +337,14 @@ macro_rules! mk_index_impls { &mut self.$field[index] } } + impl HasVectorOf<$idx> for $ty { + fn get_vector(&self) -> &Vector<$idx, Self::Output> { + &self.$field + } + fn get_vector_mut(&mut self) -> &mut Vector<$idx, Self::Output> { + &mut self.$field + } + } }; } pub(crate) use mk_index_impls; diff --git a/charon/src/ast/types/vars.rs b/charon/src/ast/types/vars.rs index 4a05f206..27931735 100644 --- a/charon/src/ast/types/vars.rs +++ b/charon/src/ast/types/vars.rs @@ -1,8 +1,12 @@ //! Type-level variables. There are 4 kinds of variables at the type-level: regions, types, const //! generics and trait clauses. The relevant definitions are in this module. -use std::ops::{Index, IndexMut}; +use std::{ + borrow::Borrow, + ops::{Index, IndexMut}, +}; use derive_generic_visitor::{Drive, DriveMut}; +use index_vec::Idx; use serde::{Deserialize, Serialize}; use crate::ast::*; @@ -284,6 +288,13 @@ impl BindingStack { pub fn depth(&self) -> DeBruijnId { DeBruijnId::new(self.stack.len() - 1) } + /// Map a bound variable to ids binding depth. + pub fn as_bound_var(&self, var: DeBruijnVar) -> (DeBruijnId, Id) { + match var { + DeBruijnVar::Bound(dbid, varid) => (dbid, varid), + DeBruijnVar::Free(varid) => (self.depth(), varid), + } + } pub fn push(&mut self, x: T) { self.stack.push(x); } @@ -292,11 +303,20 @@ impl BindingStack { } /// Helper that computes the real index into `self.stack`. fn real_index(&self, id: DeBruijnId) -> Option { - (self.stack.len() - 1).checked_sub(id.index) + self.stack.len().checked_sub(id.index + 1) } pub fn get(&self, id: DeBruijnId) -> Option<&T> { self.stack.get(self.real_index(id)?) } + pub fn get_var<'a, Id: Idx, Inner>(&'a self, var: DeBruijnVar) -> Option<&'a Inner::Output> + where + T: Borrow, + Inner: HasVectorOf + 'a, + { + let (dbid, varid) = self.as_bound_var(var); + self.get(dbid) + .and_then(|x| x.borrow().get_vector().get(varid)) + } pub fn get_mut(&mut self, id: DeBruijnId) -> Option<&mut T> { let index = self.real_index(id)?; self.stack.get_mut(index) diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index a14163c7..6d4c76ed 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -1,6 +1,8 @@ use std::borrow::Cow; use std::fmt::Display; +use index_vec::Idx; + use crate::ast::*; use crate::common::TAB_INCR; use crate::gast; @@ -255,30 +257,30 @@ impl<'a> Formatter for FmtCtx<'a> { } impl<'a> FmtCtx<'a> { - fn format_bound_var( + fn format_bound_var( &self, var: DeBruijnVar, var_prefix: &str, - get: impl Fn(&GenericParams, Id) -> Result, ()>, - ) -> String { + f: impl Fn(&T) -> Option, + ) -> String + where + GenericParams: HasVectorOf, + { if self.generics.is_empty() { return format!("{var_prefix}{var}"); } - let (dbid, varid) = match var { - DeBruijnVar::Bound(dbid, varid) => (dbid, varid), - DeBruijnVar::Free(varid) => (self.generics.depth(), varid), - }; - match self - .generics - .get(dbid) - .ok_or(()) - .and_then(|generics| get(generics, varid)) - { - Err(()) => format!("missing({var_prefix}{var})"), - Ok(v) => match v { + match self.generics.get_var::<_, GenericParams>(var) { + None => format!("missing({var_prefix}{var})"), + Some(v) => match f(v) { Some(name) => name, - None if dbid == self.generics.depth() => format!("{var_prefix}{varid}"), - None => format!("{var_prefix}{var}"), + None => { + let (dbid, varid) = self.generics.as_bound_var(var); + if dbid == self.generics.depth() { + format!("{var_prefix}{varid}") + } else { + format!("{var_prefix}{var}") + } + } }, } } @@ -286,13 +288,7 @@ impl<'a> FmtCtx<'a> { impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, var: RegionDbVar) -> String { - self.format_bound_var(var, "'_", |generics, varid| { - generics - .regions - .get(varid) - .ok_or(()) - .map(|v| v.name.as_ref().map(|name| name.to_string())) - }) + self.format_bound_var(var, "'_", |v| v.name.as_ref().map(|name| name.to_string())) } } @@ -307,33 +303,19 @@ impl<'a> Formatter<&RegionVar> for FmtCtx<'a> { impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, var: TypeDbVar) -> String { - self.format_bound_var(var, "@Type", |generics, varid| { - generics - .types - .get(varid) - .ok_or(()) - .map(|v| Some(v.to_string())) - }) + self.format_bound_var(var, "@Type", |v| Some(v.to_string())) } } impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, var: ConstGenericDbVar) -> String { - self.format_bound_var(var, "@ConstGeneric", |generics, varid| { - generics - .const_generics - .get(varid) - .ok_or(()) - .map(|v| Some(v.fmt_with_ctx(self))) - }) + self.format_bound_var(var, "@ConstGeneric", |v| Some(v.fmt_with_ctx(self))) } } impl<'a> Formatter for FmtCtx<'a> { fn format_object(&self, var: ClauseDbVar) -> String { - self.format_bound_var(var, "@TraitClause", |generics, varid| { - generics.trait_clauses.get(varid).ok_or(()).map(|_| None) - }) + self.format_bound_var(var, "@TraitClause", |_| None) } } From f644a5a92f5f3be22910623ec7e3bf756ba2f7c6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 7 Feb 2025 17:20:20 +0100 Subject: [PATCH 6/8] Fix incorrect binder usage --- charon/src/ast/types_utils.rs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 7a9c35ec..c266de8f 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -91,7 +91,7 @@ impl GenericParams { .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::bound(depth, id))), trait_refs: self.trait_clauses.map_ref_indexed(|id, clause| TraitRef { kind: TraitRefKind::Clause(DeBruijnVar::bound(depth, id)), - trait_decl_ref: clause.trait_.clone(), + trait_decl_ref: clause.trait_.clone().move_under_binders(depth), }), target, } @@ -680,10 +680,12 @@ pub trait TyVisitable: Sized + AstVisitable { /// Move under `depth` binders. fn move_under_binders(mut self, depth: DeBruijnId) -> Self { - let Continue(()) = self.visit_db_id::(|id| { - *id = id.plus(depth); - Continue(()) - }); + if !depth.is_zero() { + let Continue(()) = self.visit_db_id::(|id| { + *id = id.plus(depth); + Continue(()) + }); + } self } From da8bb6057de1d39ce1f7adf31d63abcf0d7fae4d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2025 13:28:16 +0100 Subject: [PATCH 7/8] Fix incorrect substitution of trait refs --- charon/src/ast/types_utils.rs | 10 +-- .../assoc-ty-via-supertrait-and-bounds.out | 23 +----- .../assoc-ty-via-supertrait-and-bounds.rs | 2 +- .../call-method-via-supertrait-bound.out | 66 +++++++++++++++ .../call-method-via-supertrait-bound.rs | 13 +++ .../simple/fewer-clauses-in-method-impl.out | 81 +++++++++++++------ .../ui/simple/fewer-clauses-in-method-impl.rs | 1 - 7 files changed, 145 insertions(+), 51 deletions(-) create mode 100644 charon/tests/ui/simple/call-method-via-supertrait-bound.out create mode 100644 charon/tests/ui/simple/call-method-via-supertrait-bound.rs diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index c266de8f..b3a9a936 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -141,13 +141,11 @@ impl RegionBinder { where T: AstVisitable, { - let mut val = self.skip_binder; let args = GenericArgs { regions: self.regions.map_ref_indexed(|_, _| Region::Erased), ..GenericArgs::empty(GenericsSource::Builtin) }; - val.drive_mut(&mut SubstVisitor::new(&args)); - val + self.skip_binder.substitute(&args) } } @@ -654,11 +652,11 @@ impl VisitAstMut for SubstVisitor<'_> { } } - fn exit_trait_ref(&mut self, tr: &mut TraitRef) { - match &mut tr.kind { + fn exit_trait_ref_kind(&mut self, kind: &mut TraitRefKind) { + match kind { TraitRefKind::Clause(var) => { if let Some(new_tr) = self.process_var(var) { - *tr = new_tr; + *kind = new_tr.kind; } } _ => (), diff --git a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out index 041c7ecb..20fc3624 100644 --- a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out +++ b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.out @@ -1,19 +1,4 @@ -error: Could not compute the value of Clause1_1::Clause0::Output needed to update generics <()> for item test_crate::HasOutput. - Constraints in scope: - - --> tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs:21:5 - | -21 | take::>() - | ^^^^^^^^^^^^^^^^^^^^^ - | - -error: Could not compute the value of Clause1_1::Clause0::Output needed to update generics <()> for item test_crate::HasOutput. - Constraints in scope: - - --> tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs:21:5 - | -21 | take::>() - | ^^^^^^^^^^^^^^^^^^^^^ - | - -ERROR The extraction generated 2 errors +thread 'main' panicked at src/transform/expand_associated_types.rs:920:57: +called `Option::unwrap()` on a `None` value +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace +ERROR Compilation panicked diff --git a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs index 2ffbe34b..2926344a 100644 --- a/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs +++ b/charon/tests/ui/simple/assoc-ty-via-supertrait-and-bounds.rs @@ -1,4 +1,4 @@ -//@ known-failure +//@ known-panic //@ charon-args=--remove-associated-types=* pub trait HasOutput { type Output; diff --git a/charon/tests/ui/simple/call-method-via-supertrait-bound.out b/charon/tests/ui/simple/call-method-via-supertrait-bound.out new file mode 100644 index 00000000..bf372291 --- /dev/null +++ b/charon/tests/ui/simple/call-method-via-supertrait-bound.out @@ -0,0 +1,66 @@ +# Final LLBC before serialization: + +trait test_crate::OtherTrait + +trait test_crate::ImpliesOtherTrait +{ + parent_clause0 : [@TraitClause0]: test_crate::OtherTrait +} + +trait test_crate::HasMethod +{ + fn method<'_0> = test_crate::HasMethod::method<'_0_0, Self> +} + +trait core::marker::Sized + +fn test_crate::{impl test_crate::HasMethod for T}::method<'_0, T>(@1: &'_0 (T)) +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: test_crate::OtherTrait, +{ + let @0: (); // return + let self@1: &'_ (T); // arg #1 + let @2: (); // anonymous local + + @2 := () + @0 := move (@2) + @0 := () + return +} + +impl test_crate::{impl test_crate::HasMethod for T} : test_crate::HasMethod +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: test_crate::OtherTrait, +{ + fn method<'_0> = test_crate::{impl test_crate::HasMethod for T}::method<'_0_0, T>[@TraitClause0, @TraitClause1] +} + +fn test_crate::call_method(@1: T) +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: test_crate::ImpliesOtherTrait, +{ + let @0: (); // return + let x@1: T; // arg #1 + let @2: (); // anonymous local + let @3: &'_ (T); // anonymous local + let @4: (); // anonymous local + + @3 := &x@1 + @2 := test_crate::{impl test_crate::HasMethod for T}::method<'_, T>[@TraitClause0, @TraitClause1::parent_clause0](move (@3)) + drop @3 + @fake_read(@2) + drop @2 + @4 := () + @0 := move (@4) + drop x@1 + @0 := () + return +} + +fn test_crate::HasMethod::method<'_0, Self>(@1: &'_0 (Self)) + + + diff --git a/charon/tests/ui/simple/call-method-via-supertrait-bound.rs b/charon/tests/ui/simple/call-method-via-supertrait-bound.rs new file mode 100644 index 00000000..1cc030b0 --- /dev/null +++ b/charon/tests/ui/simple/call-method-via-supertrait-bound.rs @@ -0,0 +1,13 @@ +trait OtherTrait {} +trait ImpliesOtherTrait: OtherTrait {} + +trait HasMethod { + fn method(&self); +} +impl HasMethod for T { + fn method(&self) {} +} + +fn call_method(x: T) { + let _ = x.method(); +} diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.out b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out index 1b6a6679..8f3c3db1 100644 --- a/charon/tests/ui/simple/fewer-clauses-in-method-impl.out +++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.out @@ -1,24 +1,57 @@ -error: Found inconsistent generics after transformations: - Mismatched trait clause: - expected: [@TraitClause1]: core::clone::Clone - got: core::marker::Copy<()>: core::marker::Copy<()> - Visitor stack: - charon_lib::ast::types::GenericArgs - charon_lib::ast::expressions::FnPtr - charon_lib::ast::gast::FnOperand - charon_lib::ast::gast::Call - charon_lib::ast::llbc_ast::RawStatement - charon_lib::ast::llbc_ast::Statement - alloc::vec::Vec - charon_lib::ast::llbc_ast::Block - charon_lib::ast::gast::GExprBody - charon_lib::ast::gast::Body - core::result::Result - charon_lib::ast::gast::FunDecl - --> tests/ui/simple/fewer-clauses-in-method-impl.rs:12:5 - | -12 | <() as Trait>::method::<()>() - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | - -ERROR The extraction generated 1 errors +# Final LLBC before serialization: + +trait core::marker::Sized + +trait core::clone::Clone +{ + parent_clause0 : [@TraitClause0]: core::marker::Sized + fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self> +} + +trait core::marker::Copy +{ + parent_clause0 : [@TraitClause0]: core::clone::Clone +} + +trait test_crate::Trait +{ + fn method, [@TraitClause1]: core::marker::Copy> = test_crate::Trait::method[@TraitClause0_0, @TraitClause0_1] +} + +fn test_crate::{impl test_crate::Trait for ()}::method() +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::clone::Clone, +{ + let @0: (); // return + let @1: (); // anonymous local + + @1 := () + @0 := move (@1) + @0 := () + return +} + +impl test_crate::{impl test_crate::Trait for ()} : test_crate::Trait<()> +{ + fn method, [@TraitClause1]: core::clone::Clone> = test_crate::{impl test_crate::Trait for ()}::method[@TraitClause0_0, @TraitClause0_1] +} + +fn test_crate::main() +{ + let @0: (); // return + + @0 := test_crate::{impl test_crate::Trait for ()}::method<()>[core::marker::Sized<()>, core::marker::Copy<()>]() + @0 := () + return +} + +fn test_crate::Trait::method() +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Copy, + +fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self + + + diff --git a/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs b/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs index b35a5e92..cbd9fafe 100644 --- a/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs +++ b/charon/tests/ui/simple/fewer-clauses-in-method-impl.rs @@ -1,4 +1,3 @@ -//@ known-failure //@ charon-args=--remove-associated-types=* trait Trait { fn method(); From d6a2b96cef6f05997c836d2a0431a19a64338cfa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 7 Feb 2025 14:52:21 +0100 Subject: [PATCH 8/8] check_generics: check that type variables are correctly bound --- charon/src/transform/check_generics.rs | 112 ++++++++++++------ .../ui/simple/generic-impl-with-method.out | 34 ++++++ .../ui/simple/generic-impl-with-method.rs | 7 ++ 3 files changed, 114 insertions(+), 39 deletions(-) create mode 100644 charon/tests/ui/simple/generic-impl-with-method.out create mode 100644 charon/tests/ui/simple/generic-impl-with-method.rs diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index d55b15fc..c17c5e2f 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -2,7 +2,7 @@ use derive_generic_visitor::*; use index_vec::Idx; use itertools::Itertools; -use std::{borrow::Cow, fmt::Display, mem}; +use std::{borrow::Cow, fmt::Display}; use crate::{ ast::*, @@ -16,13 +16,13 @@ use super::{ctx::TransformPass, TransformCtx}; #[derive(Visitor)] struct CheckGenericsVisitor<'a> { ctx: &'a TransformCtx, - // For pretty error printing. This can print values that we encounter because we track binders - // properly. This doesn't have the right binders to print values we get from somewhere else - // (namely `GenericParam`s). - val_fmt_ctx: FmtCtx<'a>, phase: &'static str, - // Tracks an enclosing span to make errors useful. + /// Tracks an enclosing span for error reporting. span: Span, + /// Track the binders seen so far. + // We can't keep the params by reference because the visitors don't tell us that everything + // we're visiting has lifetime `'a`. + binder_stack: BindingStack, /// Remember the names of the types visited up to here. visit_stack: Vec<&'static str>, } @@ -32,12 +32,28 @@ impl CheckGenericsVisitor<'_> { register_error!( self.ctx, self.span, - "Found inconsistent generics {}:\n{message}\nVisitor stack:\n {}", + "Found inconsistent generics {}:\n{message}\n\ + Visitor stack:\n {}\n\ + Binding stack (depth {}):\n {}", self.phase, - self.visit_stack.iter().rev().join("\n ") + self.visit_stack.iter().rev().join("\n "), + self.binder_stack.len(), + self.binder_stack + .iter_enumerated() + .map(|(i, params)| format!("{i}: {params}")) + .join("\n "), ); } + /// For pretty error printing. This can print values that we encounter because we track binders + /// properly. This doesn't have the right binders to print values we get from somewhere else + /// (namely the `GenericParam`s we get from elsewhere in the crate). + fn val_fmt_ctx(&self) -> FmtCtx<'_> { + let mut fmt = self.ctx.into_fmt(); + fmt.generics = self.binder_stack.map_ref(Cow::Borrowed); + fmt + } + fn zip_assert_match( &self, a: &Vector, @@ -73,9 +89,10 @@ impl CheckGenericsVisitor<'_> { let clause_trait_id = tclause.trait_.skip_binder.trait_id; let ref_trait_id = tref.trait_decl_ref.skip_binder.trait_id; if clause_trait_id != ref_trait_id { + let args_fmt = &self.val_fmt_ctx(); let tclause = tclause.fmt_with_ctx(params_fmt); - let tref_pred = tref.trait_decl_ref.fmt_with_ctx(&self.val_fmt_ctx); - let tref = tref.fmt_with_ctx(&self.val_fmt_ctx); + let tref_pred = tref.trait_decl_ref.fmt_with_ctx(args_fmt); + let tref = tref.fmt_with_ctx(args_fmt); self.error(format!( "Mismatched trait clause:\ \nexpected: {tclause}\ @@ -85,11 +102,12 @@ impl CheckGenericsVisitor<'_> { } fn assert_matches(&self, params_fmt: &FmtCtx<'_>, params: &GenericParams, args: &GenericArgs) { + let args_fmt = &self.val_fmt_ctx(); self.zip_assert_match( ¶ms.regions, &args.regions, params_fmt, - &self.val_fmt_ctx, + args_fmt, "regions", |_, _| {}, ); @@ -97,7 +115,7 @@ impl CheckGenericsVisitor<'_> { ¶ms.types, &args.types, params_fmt, - &self.val_fmt_ctx, + args_fmt, "type generics", |_, _| {}, ); @@ -105,7 +123,7 @@ impl CheckGenericsVisitor<'_> { ¶ms.const_generics, &args.const_generics, params_fmt, - &self.val_fmt_ctx, + args_fmt, "const generics", |_, _| {}, ); @@ -113,7 +131,7 @@ impl CheckGenericsVisitor<'_> { ¶ms.trait_clauses, &args.trait_refs, params_fmt, - &self.val_fmt_ctx, + args_fmt, "trait clauses", |tclause, tref| self.assert_clause_matches(params_fmt, tclause, tref), ); @@ -129,38 +147,53 @@ impl VisitAst for CheckGenericsVisitor<'_> { } fn visit_binder(&mut self, binder: &Binder) -> ControlFlow { - let new_fmt_ctx = self.val_fmt_ctx.push_binder(Cow::Borrowed(&binder.params)); - // Build a new `self` with a shorter `'a` because the new `'a` borrows from `binder`. - let mut new_this = CheckGenericsVisitor { - ctx: self.ctx, - val_fmt_ctx: new_fmt_ctx, - phase: self.phase, - span: self.span, - visit_stack: mem::take(&mut self.visit_stack), - }; - new_this.visit_inner(binder)?; - self.visit_stack = new_this.visit_stack; + self.binder_stack.push(binder.params.clone()); + self.visit_inner(binder)?; + self.binder_stack.pop(); Continue(()) } - fn visit_region_binder( &mut self, binder: &RegionBinder, ) -> ControlFlow { - let new_fmt_ctx = self.val_fmt_ctx.push_bound_regions(&binder.regions); - // Build a new `self` with a shorter `'a` because the new `'a` borrows from `binder`. - let mut new_this = CheckGenericsVisitor { - ctx: self.ctx, - val_fmt_ctx: new_fmt_ctx, - phase: self.phase, - span: self.span, - visit_stack: mem::take(&mut self.visit_stack), - }; - new_this.visit_inner(binder)?; - self.visit_stack = new_this.visit_stack; + self.binder_stack.push(GenericParams { + regions: binder.regions.clone(), + ..Default::default() + }); + self.visit_inner(binder)?; + self.binder_stack.pop(); Continue(()) } + fn enter_region(&mut self, x: &Region) { + if let Region::Var(var) = x { + if self.binder_stack.get_var(*var).is_none() { + self.error(format!("Found incorrect region var: {var}")); + } + } + } + fn enter_ty_kind(&mut self, x: &TyKind) { + if let TyKind::TypeVar(var) = x { + if self.binder_stack.get_var(*var).is_none() { + self.error(format!("Found incorrect type var: {var}")); + } + } + } + fn enter_const_generic(&mut self, x: &ConstGeneric) { + if let ConstGeneric::Var(var) = x { + if self.binder_stack.get_var(*var).is_none() { + self.error(format!("Found incorrect const-generic var: {var}")); + } + } + } + fn enter_trait_ref_kind(&mut self, x: &TraitRefKind) { + if let TraitRefKind::Clause(var) = x { + if self.binder_stack.get_var(*var).is_none() { + self.error(format!("Found incorrect clause var: {var}")); + } + } + } + fn visit_aggregate_kind(&mut self, agg: &AggregateKind) -> ControlFlow { match agg { AggregateKind::Adt(..) => self.visit_inner(agg)?, @@ -227,11 +260,12 @@ impl VisitAst for CheckGenericsVisitor<'_> { let fmt1 = self.ctx.into_fmt(); let tdecl_fmt = fmt1.push_binder(Cow::Borrowed(&tdecl.generics)); + let args_fmt = &self.val_fmt_ctx(); self.zip_assert_match( &tdecl.parent_clauses, &timpl.parent_trait_refs, &tdecl_fmt, - &self.val_fmt_ctx, + args_fmt, "trait parent clauses", |tclause, tref| self.assert_clause_matches(&tdecl_fmt, tclause, tref), ); @@ -289,9 +323,9 @@ impl TransformPass for Check { for item in ctx.translated.all_items() { let mut visitor = CheckGenericsVisitor { ctx, - val_fmt_ctx: ctx.into_fmt(), phase: self.0, span: item.item_meta().span, + binder_stack: BindingStack::new(item.generic_params().clone()), visit_stack: Default::default(), }; item.drive(&mut visitor); diff --git a/charon/tests/ui/simple/generic-impl-with-method.out b/charon/tests/ui/simple/generic-impl-with-method.out new file mode 100644 index 00000000..7e49226a --- /dev/null +++ b/charon/tests/ui/simple/generic-impl-with-method.out @@ -0,0 +1,34 @@ +# Final LLBC before serialization: + +trait test_crate::Trait +{ + fn method<'_0> = test_crate::Trait::method<'_0_0, Self> +} + +trait core::marker::Sized + +fn test_crate::{impl test_crate::Trait for T}::method<'_0, T>(@1: &'_0 (T)) +where + [@TraitClause0]: core::marker::Sized, +{ + let @0: (); // return + let self@1: &'_ (T); // arg #1 + let @2: (); // anonymous local + + @2 := () + @0 := move (@2) + @0 := () + return +} + +impl test_crate::{impl test_crate::Trait for T} : test_crate::Trait +where + [@TraitClause0]: core::marker::Sized, +{ + fn method<'_0> = test_crate::{impl test_crate::Trait for T}::method<'_0_0, T>[@TraitClause0] +} + +fn test_crate::Trait::method<'_0, Self>(@1: &'_0 (Self)) + + + diff --git a/charon/tests/ui/simple/generic-impl-with-method.rs b/charon/tests/ui/simple/generic-impl-with-method.rs new file mode 100644 index 00000000..7b1978a9 --- /dev/null +++ b/charon/tests/ui/simple/generic-impl-with-method.rs @@ -0,0 +1,7 @@ +pub trait Trait { + fn method(&self); +} + +impl Trait for T { + fn method(&self) {} +}