From b4c3599dad52a2d19d398b3eaa2690eb7961c064 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 19 Sep 2024 15:22:57 +0200 Subject: [PATCH] Update hax --- charon/Cargo.lock | 6 +- .../translate/translate_predicates.rs | 12 ---- .../translate/translate_traits.rs | 3 +- charon/tests/ui/ptr_to_promoted.out | 23 +++++++ .../ui/{unsupported => }/ptr_to_promoted.rs | 1 - charon/tests/ui/quantified-clause.out | 61 +++++++++++++++++++ charon/tests/ui/quantified-clause.rs | 7 +++ .../tests/ui/unsupported/ptr_to_promoted.out | 17 ------ 8 files changed, 95 insertions(+), 35 deletions(-) create mode 100644 charon/tests/ui/ptr_to_promoted.out rename charon/tests/ui/{unsupported => }/ptr_to_promoted.rs (84%) create mode 100644 charon/tests/ui/quantified-clause.out create mode 100644 charon/tests/ui/quantified-clause.rs delete mode 100644 charon/tests/ui/unsupported/ptr_to_promoted.out diff --git a/charon/Cargo.lock b/charon/Cargo.lock index a786d7e8..cd780dae 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -506,7 +506,7 @@ dependencies = [ [[package]] name = "hax-adt-into" version = "0.1.0-pre.1" -source = "git+https://github.com/hacspec/hax?branch=main#2d49e8cb4f1c7997cfab7704d14426b05f3e0c22" +source = "git+https://github.com/hacspec/hax?branch=main#ec8c2d81e8b95bc50f92dd7c7fdb943ff91bddaa" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -517,7 +517,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.1.0-pre.1" -source = "git+https://github.com/hacspec/hax?branch=main#2d49e8cb4f1c7997cfab7704d14426b05f3e0c22" +source = "git+https://github.com/hacspec/hax?branch=main#ec8c2d81e8b95bc50f92dd7c7fdb943ff91bddaa" dependencies = [ "bincode", "extension-traits", @@ -535,7 +535,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.1.0-pre.1" -source = "git+https://github.com/hacspec/hax?branch=main#2d49e8cb4f1c7997cfab7704d14426b05f3e0c22" +source = "git+https://github.com/hacspec/hax?branch=main#ec8c2d81e8b95bc50f92dd7c7fdb943ff91bddaa" dependencies = [ "bincode", "hax-adt-into", diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index cd19171c..a3584a80 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -526,18 +526,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { kind: TraitRefKind::BuiltinOrAuto(trait_decl_ref.clone()), trait_decl_ref, }, - ImplExprAtom::Todo(msg) => { - let error = format!("Error during trait resolution: {}", msg); - self.span_err(span, &error); - if !self.t_ctx.continue_on_failure() { - panic!("{}", error) - } else { - TraitRef { - kind: TraitRefKind::Unknown(msg.clone()), - trait_decl_ref, - } - } - } }; Ok(Some(trait_ref)) } diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index d8c976d7..de217c52 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -57,7 +57,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { for bound in bounds { if let rustc_middle::ty::ClauseKind::Trait(trait_pred) = bound.kind().skip_binder() { let trait_ref = bound.kind().rebind(trait_pred.trait_ref); - let trait_ref = hax::solve_trait(&self.hax_state, param_env, trait_ref); + let trait_ref = hax::solve_trait(&self.hax_state, trait_ref); let trait_ref = self.translate_trait_impl_expr(span, erase_regions, &trait_ref)?; if let Some(trait_ref) = trait_ref { trait_refs.push(trait_ref); @@ -343,7 +343,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { }; let parent_trait_refs = hax::solve_item_traits( &bt_ctx.hax_state, - tcx.param_env(rust_id), rust_trait_ref.def_id, rust_trait_ref.args, None, diff --git a/charon/tests/ui/ptr_to_promoted.out b/charon/tests/ui/ptr_to_promoted.out new file mode 100644 index 00000000..bd874d2f --- /dev/null +++ b/charon/tests/ui/ptr_to_promoted.out @@ -0,0 +1,23 @@ +# Final LLBC before serialization: + +fn test_crate::main() +{ + let @0: (); // return + let @1: *const u8; // anonymous local + let @2: usize; // anonymous local + let x@3: &'_ (u8); // local + let @4: u8; // anonymous local + let @5: &'_ (u8); // anonymous local + + @4 := const ([0]) + @5 := &@4 + x@3 := move (@5) + @1 := &raw const *(x@3) + @2 := cast<*const u8, usize>(copy (@1)) + drop @2 + @0 := () + return +} + + + diff --git a/charon/tests/ui/unsupported/ptr_to_promoted.rs b/charon/tests/ui/ptr_to_promoted.rs similarity index 84% rename from charon/tests/ui/unsupported/ptr_to_promoted.rs rename to charon/tests/ui/ptr_to_promoted.rs index cba64c98..0c72b7cc 100644 --- a/charon/tests/ui/unsupported/ptr_to_promoted.rs +++ b/charon/tests/ui/ptr_to_promoted.rs @@ -1,4 +1,3 @@ -//@ known-failure //@ charon-args=--mir_optimized fn main() { diff --git a/charon/tests/ui/quantified-clause.out b/charon/tests/ui/quantified-clause.out new file mode 100644 index 00000000..ed8e66ca --- /dev/null +++ b/charon/tests/ui/quantified-clause.out @@ -0,0 +1,61 @@ +disabled backtrace +warning[E9999]: Hax frontend found a projected type with escaping bound vars. Please report https://github.com/hacspec/hax/issues/495 + + Context: + - alias_ty: AliasTy { + args: [ + F/#0, + (&'^0.Named(test_crate::foo::'a, "'a") (),), + ], + def_id: core::ops::function::FnOnce::Output, + .. + } + - alias_kind: Projection + - trait_ref: > + - trait_ref_and_generics: ( + >, + [], + ) + - rebased_generics: [ + F/#0, + (&'^0.Named(test_crate::foo::'a, "'a") (),), + (&'^0.Named(test_crate::foo::'a, "'a") (),), + ] + - norm_rebased_generics: Ok( + >, + ) + - norm_generics: Ok( + >, + ) + - early_binder_generics: Ok( + >, + ) + - early_binder_rebased_generics: Ok( + >, + ) + | + = note: ⚠️ This is a bug in Hax's frontend. + Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! + +thread 'rustc' panicked at src/bin/charon-driver/translate/translate_types.rs:78:26: +called `Option::unwrap()` on a `None` value +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace +error: Thread panicked when extracting item `test_crate::foo`. + --> tests/ui/quantified-clause.rs:3:1 + | +3 | / fn foo(_f: F) +4 | | where +5 | | F: for<'a> FnMut(&'a ()), + | |_____________________________^ + +error: Ignoring the following item due to an error: test_crate::foo + --> tests/ui/quantified-clause.rs:3:1 + | +3 | / fn foo(_f: F) +4 | | where +5 | | F: for<'a> FnMut(&'a ()), + | |_____________________________^ + +error: aborting due to 2 previous errors; 1 warning emitted + +Error: Charon driver exited with code 101 diff --git a/charon/tests/ui/quantified-clause.rs b/charon/tests/ui/quantified-clause.rs new file mode 100644 index 00000000..f45c9c49 --- /dev/null +++ b/charon/tests/ui/quantified-clause.rs @@ -0,0 +1,7 @@ +//@ known-failure + +fn foo(_f: F) +where + F: for<'a> FnMut(&'a ()), +{ +} diff --git a/charon/tests/ui/unsupported/ptr_to_promoted.out b/charon/tests/ui/unsupported/ptr_to_promoted.out deleted file mode 100644 index 6e04ec4b..00000000 --- a/charon/tests/ui/unsupported/ptr_to_promoted.out +++ /dev/null @@ -1,17 +0,0 @@ -thread 'rustc' panicked at /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/compiler/rustc_middle/src/mir/consts.rs:510:9: -assertion `left == right` failed - left: Some(promoted[0]) - right: None -note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace -error: Thread panicked when extracting body. - --> tests/ui/unsupported/ptr_to_promoted.rs:4:1 - | -4 | / fn main() { -5 | | let x: *const u8 = &0; -6 | | let _ = x as usize; -7 | | } - | |_^ - -error: aborting due to 1 previous error - -Error: Charon driver exited with code 101