From 48b96573397077331bc84781bdde7985d16e56c7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2025 13:21:14 +0100 Subject: [PATCH 1/6] Add tests --- .../call-inherent-method-with-trait-bound.out | 94 +++++++++++++++++++ .../call-inherent-method-with-trait-bound.rs | 20 ++++ .../pass-higher-kinded-fn-item-as-closure.out | 79 ++++++++++++++++ .../pass-higher-kinded-fn-item-as-closure.rs | 9 ++ 4 files changed, 202 insertions(+) create mode 100644 charon/tests/ui/simple/call-inherent-method-with-trait-bound.out create mode 100644 charon/tests/ui/simple/call-inherent-method-with-trait-bound.rs create mode 100644 charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out create mode 100644 charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.rs diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out new file mode 100644 index 00000000..8c4b5c25 --- /dev/null +++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out @@ -0,0 +1,94 @@ +# Final LLBC before serialization: + +trait core::marker::Sized + +trait test_crate::Trait +{ + parent_clause0 : [@TraitClause0]: core::marker::Sized + type Type +} + +impl test_crate::{impl test_crate::Trait for ()} : test_crate::Trait<()> +{ + parent_clause0 = core::marker::Sized<()> + type Type = () +} + +struct test_crate::HashMap + where + [@TraitClause0]: core::marker::Sized, + = +{ + S, +} + +fn test_crate::{test_crate::HashMap[@TraitClause0]}#1::get(@1: test_crate::HashMap[@TraitClause0], @2: Q) +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: test_crate::Trait, +{ + let @0: (); // return + let _x@1: test_crate::HashMap[@TraitClause0]; // arg #1 + let _k@2: Q; // arg #2 + let @3: (); // anonymous local + + @3 := () + @0 := move (@3) + drop _k@2 + drop _x@1 + @0 := () + return +} + +fn test_crate::top_level_get(@1: test_crate::HashMap[@TraitClause0], @2: Q) +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::marker::Sized, + [@TraitClause2]: test_crate::Trait, +{ + let @0: (); // return + let _x@1: test_crate::HashMap[@TraitClause0]; // arg #1 + let _k@2: Q; // arg #2 + let @3: (); // anonymous local + + @3 := () + @0 := move (@3) + drop _k@2 + drop _x@1 + @0 := () + return +} + +fn test_crate::test(@1: test_crate::HashMap<()>[core::marker::Sized<()>]) +{ + let @0: (); // return + let map@1: test_crate::HashMap<()>[core::marker::Sized<()>]; // arg #1 + let @2: (); // anonymous local + let @3: test_crate::HashMap<()>[core::marker::Sized<()>]; // anonymous local + let @4: (); // anonymous local + let @5: (); // anonymous local + let @6: test_crate::HashMap<()>[core::marker::Sized<()>]; // anonymous local + let @7: (); // anonymous local + let @8: (); // anonymous local + + @3 := move (map@1) + @4 := () + @2 := test_crate::top_level_get<(), ()>[core::marker::Sized<()>, core::marker::Sized<()>, test_crate::{impl test_crate::Trait for ()}](move (@3), move (@4)) + drop @4 + drop @3 + drop @2 + @6 := move (map@1) + @7 := () + @5 := test_crate::{test_crate::HashMap[@TraitClause0]}#1::get<(), ()>[core::marker::Sized<()>, test_crate::{impl test_crate::Trait for ()}, core::marker::Sized<()>](move (@6), move (@7)) + drop @7 + drop @6 + drop @5 + @8 := () + @0 := move (@8) + @0 := () + return +} + + + diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.rs b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.rs new file mode 100644 index 00000000..03dfe12d --- /dev/null +++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.rs @@ -0,0 +1,20 @@ +pub trait Trait { + type Type; +} + +impl Trait for () { + type Type = (); +} + +pub struct HashMap(S); + +impl HashMap { + pub fn get(_x: HashMap, _k: Q) {} +} + +pub fn top_level_get(_x: HashMap, _k: Q) {} + +pub fn test(map: HashMap<()>) { + top_level_get(map, ()); + HashMap::get(map, ()); +} diff --git a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out new file mode 100644 index 00000000..e1dd7e77 --- /dev/null +++ b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.out @@ -0,0 +1,79 @@ +# Final LLBC before serialization: + +fn test_crate::flabada<'a>(@1: &'a (())) -> &'a (()) +{ + let @0: &'_ (()); // return + let x@1: &'_ (()); // arg #1 + + @0 := copy (x@1) + return +} + +trait core::marker::Sized + +trait core::marker::Tuple + +trait core::ops::function::FnOnce +{ + parent_clause0 : [@TraitClause0]: core::marker::Sized + parent_clause1 : [@TraitClause1]: core::marker::Tuple + parent_clause2 : [@TraitClause2]: core::marker::Sized + type Output + fn call_once = core::ops::function::FnOnce::call_once +} + +trait core::ops::function::FnMut +{ + parent_clause0 : [@TraitClause0]: core::ops::function::FnOnce + parent_clause1 : [@TraitClause1]: core::marker::Sized + parent_clause2 : [@TraitClause2]: core::marker::Tuple + fn call_mut<'_0> = core::ops::function::FnMut::call_mut<'_0_0, Self, Args> +} + +trait core::ops::function::Fn +{ + parent_clause0 : [@TraitClause0]: core::ops::function::FnMut + parent_clause1 : [@TraitClause1]: core::marker::Sized + parent_clause2 : [@TraitClause2]: core::marker::Tuple + fn call<'_0> = core::ops::function::Fn::call<'_0_0, Self, Args> +} + +fn test_crate::call<'b, F>(@1: F) +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: core::ops::function::Fn, + @TraitClause1::parent_clause0::parent_clause0::Output = &'b (()), +{ + let @0: (); // return + let @1: F; // arg #1 + let @2: (); // anonymous local + + @2 := () + @0 := move (@2) + drop @1 + @0 := () + return +} + +fn test_crate::flibidi() +{ + let @0: (); // return + let @1: (); // anonymous local + let @2: (); // anonymous local + + @1 := test_crate::call<'_, fn<'a>(&'a (())) -> &'a (())>[core::marker::Sized(&'a (())) -> &'a (())>, core::ops::function::Fn(&'a (())) -> &'a (()), (&'_ (()))>](const (test_crate::flabada<'_>)) + drop @1 + @2 := () + @0 := move (@2) + @0 := () + return +} + +fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> Self::parent_clause0::parent_clause0::Output + +fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> Self::parent_clause0::Output + +fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> Self::Output + + + diff --git a/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.rs b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.rs new file mode 100644 index 00000000..a91f9716 --- /dev/null +++ b/charon/tests/ui/simple/pass-higher-kinded-fn-item-as-closure.rs @@ -0,0 +1,9 @@ +pub fn flabada<'a>(x: &'a ()) -> &'a () { + x +} + +pub fn call<'b, F: Fn(&'b ()) -> &'b ()>(_: F) {} + +pub fn flibidi() { + call(flabada); +} From f5a2bde95dd01c2b0e6290a12a98aedbedc00a7c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 16 Jan 2025 16:20:25 +0100 Subject: [PATCH 2/6] Print command on test failure --- charon/tests/ui.rs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/charon/tests/ui.rs b/charon/tests/ui.rs index 0eb6bb21..1d844bf3 100644 --- a/charon/tests/ui.rs +++ b/charon/tests/ui.rs @@ -7,10 +7,12 @@ use anyhow::{anyhow, bail}; use assert_cmd::prelude::{CommandCargoExt, OutputAssertExt}; use indoc::indoc as unindent; +use itertools::Itertools; use libtest_mimic::Trial; use snapbox::filter::Filter as _; use std::{ error::Error, + ffi::OsStr, fs::read_to_string, path::{Path, PathBuf}, process::Command, @@ -204,6 +206,10 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> { for arg in &test_case.magic_comments.charon_opts { cmd.arg(arg); } + let cmd_str = format!( + "charon {}", + cmd.get_args().map(OsStr::to_string_lossy).join(" ") + ); let output = cmd.output()?; let stderr = String::from_utf8(output.stderr.clone())?; @@ -217,7 +223,7 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> { } else { "errored" }; - bail!("Compilation was expected to panic but instead {status}: {stderr}"); + bail!("Command: `{cmd_str}`\nCompilation was expected to panic but instead {status}:\n{stderr}"); } stderr } @@ -228,7 +234,7 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> { } else { "panicked" }; - bail!("Compilation was expected to fail but instead {status}: {stderr}"); + bail!("Command: `{cmd_str}`\nCompilation was expected to fail but instead {status}:\n{stderr}"); } stderr } @@ -240,7 +246,7 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> { let actual = snapbox::filter::FilterNewlines.filter(actual); actual.write_to_path(&test_case.expected)?; } - bail!("Compilation failed: {stderr}") + bail!("Command: `{cmd_str}`\nCompilation failed:\n{stderr}") } stdout } From c7df271a6d1ecde8561136d1ef138ed5af37b285 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2025 15:55:56 +0100 Subject: [PATCH 3/6] Update hax --- charon/Cargo.lock | 6 +-- charon/Cargo.toml | 3 +- charon/tests/ui/closures.out | 2 +- charon/tests/ui/issue-165-vec-macro.out | 4 +- .../tests/ui/issue-4-slice-try-into-array.out | 2 +- charon/tests/ui/issue-4-traits.out | 2 +- charon/tests/ui/issue-45-misc.out | 2 +- charon/tests/ui/polonius_map.out | 38 +++++++++---------- charon/tests/ui/result-unwrap.out | 2 +- .../call-inherent-method-with-trait-bound.out | 2 +- 10 files changed, 32 insertions(+), 31 deletions(-) diff --git a/charon/Cargo.lock b/charon/Cargo.lock index d0a716bc..173ad5e1 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -818,7 +818,7 @@ dependencies = [ [[package]] name = "hax-adt-into" version = "0.1.0-rc.1" -source = "git+https://github.com/cryspen/hax?branch=main#54a4159b0e7ccc8dd4fdd811a239bc271145efcb" +source = "git+https://github.com/Nadrieril/hax?branch=fix-clause-order#591da2b985d7c2e1388c5e1ad595f225c90ab90e" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -829,7 +829,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.1.0-rc.1" -source = "git+https://github.com/cryspen/hax?branch=main#54a4159b0e7ccc8dd4fdd811a239bc271145efcb" +source = "git+https://github.com/Nadrieril/hax?branch=fix-clause-order#591da2b985d7c2e1388c5e1ad595f225c90ab90e" dependencies = [ "extension-traits", "hax-adt-into", @@ -846,7 +846,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.1.0-rc.1" -source = "git+https://github.com/cryspen/hax?branch=main#54a4159b0e7ccc8dd4fdd811a239bc271145efcb" +source = "git+https://github.com/Nadrieril/hax?branch=fix-clause-order#591da2b985d7c2e1388c5e1ad595f225c90ab90e" dependencies = [ "hax-adt-into", "schemars", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 3346f5bf..6327dbab 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -78,7 +78,8 @@ tracing = { version = "0.1", features = [ "max_level_trace" ] } wait-timeout = { version = "0.2.0", optional = true } which = "7.0" -hax-frontend-exporter = { git = "https://github.com/cryspen/hax", branch = "main", optional = true } +# hax-frontend-exporter = { git = "https://github.com/cryspen/hax", branch = "main", optional = true } +hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "fix-clause-order", optional = true } # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true } macros = { path = "./macros" } diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index ccd5b1d7..e5580948 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -685,7 +685,7 @@ fn test_crate::test_array_map(@1: Array) -> Array}#23::map i32, i32, 256 : usize>[core::marker::Sized i32>, core::marker::Sized, core::ops::function::FnMut i32, (i32)>, core::marker::Sized](move (@2), move (@3)) + @0 := core::array::{Array}#23::map i32, i32, 256 : usize>[core::marker::Sized, core::marker::Sized i32>, core::marker::Sized, core::ops::function::FnMut i32, (i32)>](move (@2), move (@3)) drop @3 drop @2 return diff --git a/charon/tests/ui/issue-165-vec-macro.out b/charon/tests/ui/issue-165-vec-macro.out index fef93285..4d2a57fc 100644 --- a/charon/tests/ui/issue-165-vec-macro.out +++ b/charon/tests/ui/issue-165-vec-macro.out @@ -53,7 +53,7 @@ fn test_crate::foo() drop @4 drop @4 drop @3 - _v@1 := alloc::slice::{Slice}::into_vec[core::marker::Sized, core::marker::Sized](move (@2)) + _v@1 := alloc::slice::{Slice}::into_vec[core::marker::Sized, core::marker::Sized](move (@2)) drop @2 @fake_read(_v@1) _v2@5 := alloc::vec::from_elem[core::marker::Sized, core::clone::impls::{impl core::clone::Clone for i32}#14](const (1 : i32), const (10 : usize)) @@ -91,7 +91,7 @@ fn test_crate::bar() drop @4 drop @4 drop @3 - @1 := alloc::slice::{Slice}::into_vec[core::marker::Sized, core::marker::Sized](move (@2)) + @1 := alloc::slice::{Slice}::into_vec[core::marker::Sized, core::marker::Sized](move (@2)) drop @2 @fake_read(@1) drop @1 diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out index 8b1b6dce..4465c483 100644 --- a/charon/tests/ui/issue-4-slice-try-into-array.out +++ b/charon/tests/ui/issue-4-slice-try-into-array.out @@ -106,7 +106,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice)) @4 := &*(s@1) @3 := core::convert::{impl core::convert::TryInto for T}#6::try_into<&'_ (Slice), Array>[core::marker::Sized<&'_ (Slice)>, core::marker::Sized>, core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array}#7<'_, u8, 4 : usize>[core::marker::Sized, core::marker::{impl core::marker::Copy for u8}#38]](move (@4)) drop @4 - _array@2 := core::result::{core::result::Result[@TraitClause0, @TraitClause1]}::unwrap, core::array::TryFromSliceError>[core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26, core::marker::Sized>, core::marker::Sized](move (@3)) + _array@2 := core::result::{core::result::Result[@TraitClause0, @TraitClause1]}::unwrap, core::array::TryFromSliceError>[core::marker::Sized>, core::marker::Sized, core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26](move (@3)) drop @3 @fake_read(_array@2) @5 := () diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out index 8b1b6dce..4465c483 100644 --- a/charon/tests/ui/issue-4-traits.out +++ b/charon/tests/ui/issue-4-traits.out @@ -106,7 +106,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice)) @4 := &*(s@1) @3 := core::convert::{impl core::convert::TryInto for T}#6::try_into<&'_ (Slice), Array>[core::marker::Sized<&'_ (Slice)>, core::marker::Sized>, core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array}#7<'_, u8, 4 : usize>[core::marker::Sized, core::marker::{impl core::marker::Copy for u8}#38]](move (@4)) drop @4 - _array@2 := core::result::{core::result::Result[@TraitClause0, @TraitClause1]}::unwrap, core::array::TryFromSliceError>[core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26, core::marker::Sized>, core::marker::Sized](move (@3)) + _array@2 := core::result::{core::result::Result[@TraitClause0, @TraitClause1]}::unwrap, core::array::TryFromSliceError>[core::marker::Sized>, core::marker::Sized, core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26](move (@3)) drop @3 @fake_read(_array@2) @5 := () diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 21e28f33..68927cae 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -48,7 +48,7 @@ fn test_crate::map(@1: Array) -> Array @2 := copy (x@1) @3 := {test_crate::map::closure} {} - @0 := core::array::{Array}#23::map i32, i32, 256 : usize>[core::marker::Sized i32>, core::marker::Sized, core::ops::function::FnMut i32, (i32)>, core::marker::Sized](move (@2), move (@3)) + @0 := core::array::{Array}#23::map i32, i32, 256 : usize>[core::marker::Sized, core::marker::Sized i32>, core::marker::Sized, core::ops::function::FnMut i32, (i32)>](move (@2), move (@3)) drop @3 drop @2 return diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out index b9eaaeda..6a3d448d 100644 --- a/charon/tests/ui/polonius_map.out +++ b/charon/tests/ui/polonius_map.out @@ -82,11 +82,19 @@ where [@TraitClause7]: core::hash::Hash, [@TraitClause8]: core::cmp::Eq, -fn core::borrow::{impl core::borrow::Borrow for T}::borrow<'_0, T>(@1: &'_0 (T)) -> &'_0 (T) +fn core::cmp::impls::{impl core::cmp::PartialEq for u32}#24::eq<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool -impl core::borrow::{impl core::borrow::Borrow for T} : core::borrow::Borrow +fn core::cmp::impls::{impl core::cmp::PartialEq for u32}#24::ne<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool + +impl core::cmp::impls::{impl core::cmp::PartialEq for u32}#24 : core::cmp::PartialEq { - fn borrow<'_0> = core::borrow::{impl core::borrow::Borrow for T}::borrow<'_0_0, T> + fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq for u32}#24::eq<'_0_0, '_0_1> + fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq for u32}#24::ne<'_0_0, '_0_1> +} + +impl core::cmp::impls::{impl core::cmp::Eq for u32}#43 : core::cmp::Eq +{ + parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u32}#24 } fn core::hash::impls::{impl core::hash::Hash for u32}#11::hash<'_0, '_1, H>(@1: &'_0 (u32), @2: &'_1 mut (H)) @@ -105,21 +113,6 @@ impl core::hash::impls::{impl core::hash::Hash for u32}#11 : core::hash::Hash, [@TraitClause1]: core::hash::Hasher> = core::hash::impls::{impl core::hash::Hash for u32}#11::hash_slice<'_0_0, '_0_1, H>[@TraitClause0_0, @TraitClause0_1] } -fn core::cmp::impls::{impl core::cmp::PartialEq for u32}#24::eq<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool - -fn core::cmp::impls::{impl core::cmp::PartialEq for u32}#24::ne<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool - -impl core::cmp::impls::{impl core::cmp::PartialEq for u32}#24 : core::cmp::PartialEq -{ - fn eq<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq for u32}#24::eq<'_0_0, '_0_1> - fn ne<'_0, '_1> = core::cmp::impls::{impl core::cmp::PartialEq for u32}#24::ne<'_0_0, '_0_1> -} - -impl core::cmp::impls::{impl core::cmp::Eq for u32}#43 : core::cmp::Eq -{ - parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u32}#24 -} - opaque type std::hash::random::DefaultHasher fn std::hash::random::{impl core::hash::Hasher for std::hash::random::DefaultHasher}#4::finish<'_0>(@1: &'_0 (std::hash::random::DefaultHasher)) -> u64 @@ -145,6 +138,13 @@ impl std::hash::random::{impl core::hash::BuildHasher for std::hash::random::Ran fn build_hasher<'_0> = std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState}#1::build_hasher<'_0_0> } +fn core::borrow::{impl core::borrow::Borrow for T}::borrow<'_0, T>(@1: &'_0 (T)) -> &'_0 (T) + +impl core::borrow::{impl core::borrow::Borrow for T} : core::borrow::Borrow +{ + fn borrow<'_0> = core::borrow::{impl core::borrow::Borrow for T}::borrow<'_0_0, T> +} + fn std::collections::hash::map::{std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]}#2::insert<'_0, K, V, S>(@1: &'_0 mut (std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]), @2: K, @3: V) -> core::option::Option[@TraitClause1] where [@TraitClause0]: core::marker::Sized, @@ -195,7 +195,7 @@ fn test_crate::get_or_insert<'_0>(@1: &'_0 mut (std::collections::hash::map::Has @6 := const (22 : u32) @5 := &@6 @4 := &*(@5) - @2 := std::collections::hash::map::{std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]}#2::get<'_, '_, u32, u32, std::hash::random::RandomState, u32>[core::borrow::{impl core::borrow::Borrow for T}, core::hash::impls::{impl core::hash::Hash for u32}#11, core::cmp::impls::{impl core::cmp::Eq for u32}#43, core::marker::Sized, core::marker::Sized, core::marker::Sized, core::cmp::impls::{impl core::cmp::Eq for u32}#43, core::hash::impls::{impl core::hash::Hash for u32}#11, std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState}#1](move (@3), move (@4)) + @2 := std::collections::hash::map::{std::collections::hash::map::HashMap[@TraitClause0, @TraitClause1, @TraitClause2]}#2::get<'_, '_, u32, u32, std::hash::random::RandomState, u32>[core::marker::Sized, core::marker::Sized, core::marker::Sized, core::cmp::impls::{impl core::cmp::Eq for u32}#43, core::hash::impls::{impl core::hash::Hash for u32}#11, std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState}#1, core::borrow::{impl core::borrow::Borrow for T}, core::hash::impls::{impl core::hash::Hash for u32}#11, core::cmp::impls::{impl core::cmp::Eq for u32}#43](move (@3), move (@4)) drop @4 drop @3 @fake_read(@2) diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out index 12c61e5d..028dfea4 100644 --- a/charon/tests/ui/result-unwrap.out +++ b/charon/tests/ui/result-unwrap.out @@ -132,7 +132,7 @@ fn test_crate::unwrap(@1: core::result::Result[core::marker::Sized[core::marker::Sized, core::marker::Sized]; // anonymous local @2 := copy (res@1) - @0 := core::result::{core::result::Result[@TraitClause0, @TraitClause1]}::unwrap[core::fmt::num::{impl core::fmt::Debug for u32}#86, core::marker::Sized, core::marker::Sized](move (@2)) + @0 := core::result::{core::result::Result[@TraitClause0, @TraitClause1]}::unwrap[core::marker::Sized, core::marker::Sized, core::fmt::num::{impl core::fmt::Debug for u32}#86](move (@2)) drop @2 return } diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out index 8c4b5c25..21e85f48 100644 --- a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out +++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out @@ -80,7 +80,7 @@ fn test_crate::test(@1: test_crate::HashMap<()>[core::marker::Sized<()>]) drop @2 @6 := move (map@1) @7 := () - @5 := test_crate::{test_crate::HashMap[@TraitClause0]}#1::get<(), ()>[core::marker::Sized<()>, test_crate::{impl test_crate::Trait for ()}, core::marker::Sized<()>](move (@6), move (@7)) + @5 := test_crate::{test_crate::HashMap[@TraitClause0]}#1::get<(), ()>[core::marker::Sized<()>, core::marker::Sized<()>, test_crate::{impl test_crate::Trait for ()}](move (@6), move (@7)) drop @7 drop @6 drop @5 From 957a2d992f7e4c2bab2fc6ecfe2bbeedaea5f5d0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2025 14:15:29 +0100 Subject: [PATCH 4/6] Tweak printing code --- charon/src/pretty/fmt_with_ctx.rs | 134 ++++++++++++++---------------- charon/src/pretty/formatter.rs | 2 +- 2 files changed, 65 insertions(+), 71 deletions(-) diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index fe4b0543..e617e86a 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -11,7 +11,7 @@ use crate::{ use itertools::Itertools; use std::{ borrow::Cow, - fmt::{self, Display, Write}, + fmt::{self, Debug, Display, Write}, }; /// Format the AST type as a string. @@ -185,6 +185,13 @@ impl FmtWithCtx for ConstGeneric { } } +impl FmtWithCtx for ConstGenericVar { + fn fmt_with_ctx(&self, ctx: &C) -> String { + let ty = self.ty.fmt_with_ctx(ctx); + format!("const {} : {}", self.name, ty) + } +} + impl FmtWithCtx for DeclarationGroup { fn fmt_with_ctx(&self, ctx: &C) -> String { use DeclarationGroup::*; @@ -369,9 +376,9 @@ impl GenericParams { where C: AstFormatter, { - let regions = self.regions.iter().map(|x| ctx.format_object(x)); - let types = self.types.iter().map(|x| x.to_string()); - let const_generics = self.const_generics.iter().map(|x| x.to_string()); + let regions = self.regions.iter().map(|x| x.fmt_with_ctx(ctx)); + let types = self.types.iter().map(|x| x.fmt_with_ctx(ctx)); + let const_generics = self.const_generics.iter().map(|x| x.fmt_with_ctx(ctx)); regions.chain(types).chain(const_generics) } @@ -606,6 +613,17 @@ impl FmtWithCtx for ImplElem { } } +impl FmtWithCtx for LiteralTy { + fn fmt_with_ctx(&self, _ctx: &C) -> String { + match self { + LiteralTy::Integer(ty) => ty.to_string(), + LiteralTy::Float(ty) => ty.to_string(), + LiteralTy::Char => "char".to_owned(), + LiteralTy::Bool => "bool".to_owned(), + } + } +} + impl FmtWithCtx for Name { fn fmt_with_ctx(&self, ctx: &C) -> String { let name = self @@ -828,6 +846,12 @@ impl RegionBinder { } } +impl FmtWithCtx for RegionVar { + fn fmt_with_ctx(&self, ctx: &C) -> String { + ctx.format_object(self) + } +} + impl FmtWithCtx for Rvalue { fn fmt_with_ctx(&self, ctx: &C) -> String { match self { @@ -1444,6 +1468,12 @@ impl FmtWithCtx for TypeId { } } +impl FmtWithCtx for TypeVar { + fn fmt_with_ctx(&self, _ctx: &C) -> String { + self.name.to_string() + } +} + impl FmtWithCtx for UnOp { fn fmt_with_ctx(&self, ctx: &C) -> String { match self { @@ -1596,30 +1626,12 @@ impl std::fmt::Display for IntegerTy { } } -impl std::fmt::Display for GenericArgs { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { - write!(f, "{}", self.fmt_with_ctx(&FmtCtx::new())) - } -} - impl std::fmt::Display for GenericParams { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { write!(f, "{}", self.fmt_with_ctx_single_line(&FmtCtx::new())) } } -impl std::fmt::Debug for GenericArgs { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { - write!(f, "{}", self) - } -} - -impl std::fmt::Debug for GenericParams { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { - write!(f, "{}", self) - } -} - impl std::fmt::Display for Literal { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { match self { @@ -1633,35 +1645,12 @@ impl std::fmt::Display for Literal { } } -impl std::fmt::Display for LiteralTy { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { - match self { - LiteralTy::Integer(ty) => ty.fmt(f), - LiteralTy::Float(ty) => ty.fmt(f), - LiteralTy::Char => write!(f, "char"), - LiteralTy::Bool => write!(f, "bool"), - } - } -} - impl std::fmt::Display for Loc { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { write!(f, "{}:{}", self.line, self.col) } } -impl std::fmt::Display for Operand { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { - write!(f, "{}", self.fmt_with_ctx(&FmtCtx::new())) - } -} - -impl std::fmt::Display for Place { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { - write!(f, "{}", self.fmt_with_ctx(&FmtCtx::new())) - } -} - impl std::fmt::Display for RawAttribute { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { write!(f, "{}", self.path)?; @@ -1672,12 +1661,6 @@ impl std::fmt::Display for RawAttribute { } } -impl std::fmt::Display for Rvalue { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { - write!(f, "{}", self.fmt_with_ctx(&FmtCtx::new())) - } -} - impl std::fmt::Display for ScalarValue { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), std::fmt::Error> { match self { @@ -1715,21 +1698,9 @@ impl std::fmt::Display for TraitItemName { } } -impl std::string::ToString for ConstGenericVar { - fn to_string(&self) -> String { - format!("const {} : {}", self.name, self.ty.to_string()) - } -} - -impl std::string::ToString for Field { - fn to_string(&self) -> String { - self.fmt_with_ctx(&FmtCtx::new()) - } -} - -impl std::string::ToString for TypeVar { - fn to_string(&self) -> String { - self.name.to_string() +impl std::fmt::Display for TypeVar { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.name) } } @@ -1745,11 +1716,34 @@ impl std::string::ToString for Var { } } -impl std::string::ToString for Variant { - fn to_string(&self) -> String { - self.fmt_with_ctx(&FmtCtx::new()) - } +macro_rules! impl_display_via_ctx { + ($ty:ty) => { + impl Display for $ty { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str(&self.fmt_with_ctx(&FmtCtx::new())) + } + } + }; } +macro_rules! impl_debug_via_display { + ($ty:ty) => { + impl Debug for $ty { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + <_ as Display>::fmt(self, f) + } + } + }; +} + +impl_display_via_ctx!(Field); +impl_display_via_ctx!(GenericArgs); +impl_display_via_ctx!(LiteralTy); +impl_display_via_ctx!(Operand); +impl_display_via_ctx!(Place); +impl_display_via_ctx!(Rvalue); +impl_display_via_ctx!(Variant); +impl_debug_via_display!(GenericArgs); +impl_debug_via_display!(GenericParams); /// Format a function call. /// We return the pair: (function call, comment) diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index 1537866e..a707b5be 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -322,7 +322,7 @@ impl<'a> Formatter for FmtCtx<'a> { .and_then(|generics| generics.const_generics.get(varid)) { None => format!("missing_cg_var({var})"), - Some(v) => v.to_string(), + Some(v) => v.fmt_with_ctx(self), } } } From 1f48222d03aeba2a75115230ae352c6d14a139ae Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2025 14:23:00 +0100 Subject: [PATCH 5/6] Add more details to check_generics errors --- charon/src/transform/check_generics.rs | 183 ++++++++++++++++++++++--- 1 file changed, 165 insertions(+), 18 deletions(-) diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index 8e814ee3..eb7f9a79 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -1,15 +1,25 @@ //! Check that all supplied generic types match the corresponding generic parameters. use derive_generic_visitor::*; +use index_vec::Idx; use itertools::Itertools; -use std::fmt::Display; +use std::{borrow::Cow, fmt::Display, mem}; -use crate::{llbc_ast::*, register_error}; +use crate::{ + ast::*, + formatter::{FmtCtx, IntoFormatter, PushBinder}, + pretty::FmtWithCtx, + register_error, +}; 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. span: Span, @@ -27,6 +37,76 @@ impl CheckGenericsVisitor<'_> { self.visit_stack.iter().rev().join("\n ") ); } + + fn zip_assert_match( + &self, + a: &Vector, + b: &Vector, + a_fmt: &FmtA, + b_fmt: &FmtB, + kind: &str, + check_inner: impl Fn(&A, &B), + ) where + I: Idx, + A: for<'a> FmtWithCtx, + B: for<'a> FmtWithCtx, + { + if a.len() == b.len() { + a.iter().zip(b.iter()).for_each(|(x, y)| check_inner(x, y)); + } else { + let a = a.iter().map(|x| x.fmt_with_ctx(a_fmt)).join(", "); + let b = b.iter().map(|x| x.fmt_with_ctx(b_fmt)).join(", "); + self.error(format!( + "Mismatched {kind}:\ + \nexpected: [{a}]\ + \n got: [{b}]" + )) + } + } + + fn assert_clause_matches( + &self, + _params_fmt: &FmtCtx<'_>, + _tclause: &TraitClause, + _tref: &TraitRef, + ) { + // TODO + } + + fn assert_matches(&self, params_fmt: &FmtCtx<'_>, params: &GenericParams, args: &GenericArgs) { + self.zip_assert_match( + ¶ms.regions, + &args.regions, + params_fmt, + &self.val_fmt_ctx, + "regions", + |_, _| {}, + ); + self.zip_assert_match( + ¶ms.types, + &args.types, + params_fmt, + &self.val_fmt_ctx, + "type generics", + |_, _| {}, + ); + self.zip_assert_match( + ¶ms.const_generics, + &args.const_generics, + params_fmt, + &self.val_fmt_ctx, + "const generics", + |_, _| {}, + ); + self.zip_assert_match( + ¶ms.trait_clauses, + &args.trait_refs, + params_fmt, + &self.val_fmt_ctx, + "trait clauses", + |tclause, tref| self.assert_clause_matches(params_fmt, tclause, tref), + ); + } } impl VisitAst for CheckGenericsVisitor<'_> { @@ -37,6 +117,39 @@ impl VisitAst for CheckGenericsVisitor<'_> { Continue(()) } + 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; + 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; + Continue(()) + } + fn visit_aggregate_kind(&mut self, agg: &AggregateKind) -> ControlFlow { match agg { AggregateKind::Adt(..) => self.visit_inner(agg)?, @@ -52,12 +165,17 @@ impl VisitAst for CheckGenericsVisitor<'_> { } fn enter_generic_args(&mut self, args: &GenericArgs) { - let params = match &args.target { + let fmt1; + let fmt2; + let (params, params_fmt) = match &args.target { GenericsSource::Item(item_id) => { let Some(item) = self.ctx.translated.get_item(*item_id) else { return; }; - item.generic_params() + let params = item.generic_params(); + fmt1 = self.ctx.into_fmt(); + let fmt = fmt1.push_binder(Cow::Borrowed(params)); + (params, fmt) } GenericsSource::Method(trait_id, method_name) => { let Some(trait_decl) = self.ctx.translated.trait_decls.get(*trait_id) else { @@ -71,15 +189,15 @@ impl VisitAst for CheckGenericsVisitor<'_> { else { return; }; - &bound_fn.params + let params = &bound_fn.params; + fmt1 = self.ctx.into_fmt(); + fmt2 = fmt1.push_binder(Cow::Borrowed(&trait_decl.generics)); + let fmt = fmt2.push_binder(Cow::Borrowed(params)); + (params, fmt) } GenericsSource::Builtin => return, }; - if !args.matches(params) { - self.error(format!( - "Mismatched generics:\nexpected: {params:?}\n got: {args:?}" - )) - } + self.assert_matches(¶ms_fmt, params, args); } // Special case that is not represented as a `GenericArgs`. @@ -96,18 +214,37 @@ impl VisitAst for CheckGenericsVisitor<'_> { assert!(timpl.type_clauses.is_empty()); assert!(tdecl.type_clauses.is_empty()); - let args_match = timpl.parent_trait_refs.len() == tdecl.parent_clauses.len() - && timpl.types.len() == tdecl.types.len() - && timpl.consts.len() == tdecl.consts.len(); - // Check that type names match. - let args_match = args_match + let fmt1 = self.ctx.into_fmt(); + let tdecl_fmt = fmt1.push_binder(Cow::Borrowed(&tdecl.generics)); + self.zip_assert_match( + &tdecl.parent_clauses, + &timpl.parent_trait_refs, + &tdecl_fmt, + &self.val_fmt_ctx, + "trait parent clauses", + |tclause, tref| self.assert_clause_matches(&tdecl_fmt, tclause, tref), + ); + let types_match = timpl.types.len() == tdecl.types.len() && tdecl .types .iter() .zip(timpl.types.iter()) .all(|(dname, (iname, _))| dname == iname); - if !args_match { - self.error("The generics supplied by the trait impl don't match the trait decl.") + if !types_match { + self.error( + "The associated types supplied by the trait impl don't match the trait decl.", + ) + } + let consts_match = timpl.consts.len() == tdecl.consts.len() + && tdecl + .types + .iter() + .zip(timpl.types.iter()) + .all(|(dname, (iname, _))| dname == iname); + if !consts_match { + self.error( + "The associated consts supplied by the trait impl don't match the trait decl.", + ) } let methods = timpl.required_methods.len() == tdecl.required_methods.len(); if !methods { @@ -115,7 +252,16 @@ impl VisitAst for CheckGenericsVisitor<'_> { } } - fn visit_llbc_statement(&mut self, st: &Statement) -> ControlFlow { + fn visit_ullbc_statement(&mut self, st: &ullbc_ast::Statement) -> ControlFlow { + // Track span for more precise error messages. + let old_span = self.span; + self.span = st.span; + self.visit_inner(st)?; + self.span = old_span; + Continue(()) + } + + fn visit_llbc_statement(&mut self, st: &llbc_ast::Statement) -> ControlFlow { // Track span for more precise error messages. let old_span = self.span; self.span = st.span; @@ -132,6 +278,7 @@ 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, visit_stack: Default::default(), From 2315e2d71eb1ee8c375d504f65af779f7cf73e15 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2025 15:12:11 +0100 Subject: [PATCH 6/6] Check that trait references are for the correct trait --- charon/src/transform/check_generics.rs | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index eb7f9a79..d55b15fc 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -66,11 +66,22 @@ impl CheckGenericsVisitor<'_> { fn assert_clause_matches( &self, - _params_fmt: &FmtCtx<'_>, - _tclause: &TraitClause, - _tref: &TraitRef, + params_fmt: &FmtCtx<'_>, + tclause: &TraitClause, + tref: &TraitRef, ) { - // TODO + 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 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); + self.error(format!( + "Mismatched trait clause:\ + \nexpected: {tclause}\ + \n got: {tref}: {tref_pred}" + )); + } } fn assert_matches(&self, params_fmt: &FmtCtx<'_>, params: &GenericParams, args: &GenericArgs) {