From a1566c06bc3d4e8642c5882104f9ca47f0f15eb3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 15 Oct 2024 17:30:30 +0200 Subject: [PATCH] Improve some error messages --- .../charon-driver/translate/translate_ctx.rs | 5 +++ .../translate/translate_functions_to_ullbc.rs | 32 ++++++++++++------- .../translate/translate_predicates.rs | 9 +++++- .../translate/translate_types.rs | 6 +++- charon/src/transform/hide_marker_traits.rs | 3 +- charon/tests/ui/error-dependencies.rs | 2 +- charon/tests/ui/issue-378-ctor-as-fn.out | 16 ++++++++-- .../tests/ui/unsupported/unbound-lifetime.out | 12 +++---- .../tests/ui/unsupported/unbound-lifetime.rs | 1 + .../ui/unsupported/well-formedness-bound.out | 2 +- 10 files changed, 63 insertions(+), 25 deletions(-) diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 3f96eeb7..3a41944c 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -397,6 +397,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // block. None } + DefPathData::Ctor => { + // Do nothing, the constructor of a struct/variant has the same name as the + // struct/variant. + None + } _ => { error_or_panic!( self, diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index dbe20cac..edf99a90 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs @@ -55,14 +55,6 @@ fn translate_borrow_kind(borrow_kind: hax::BorrowKind) -> BorrowKind { } } -fn translate_unaryop_kind(binop: hax::UnOp) -> UnOp { - match binop { - hax::UnOp::Not => UnOp::Not, - hax::UnOp::Neg => UnOp::Neg, - hax::UnOp::PtrMetadata => unimplemented!("Unop::PtrMetadata"), - } -} - impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { fn translate_binaryop_kind(&mut self, span: Span, binop: hax::BinOp) -> Result { Ok(match binop { @@ -601,10 +593,19 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { }; Ok(Rvalue::NullaryOp(op, ty)) } - hax::Rvalue::UnaryOp(unop, operand) => Ok(Rvalue::UnaryOp( - translate_unaryop_kind(*unop), - self.translate_operand(span, operand)?, - )), + hax::Rvalue::UnaryOp(unop, operand) => { + let unop = match unop { + hax::UnOp::Not => UnOp::Not, + hax::UnOp::Neg => UnOp::Neg, + hax::UnOp::PtrMetadata => { + error_or_panic!(self, span, "Unsupported operation: PtrMetadata") + } + }; + Ok(Rvalue::UnaryOp( + unop, + self.translate_operand(span, operand)?, + )) + } hax::Rvalue::Discriminant(place) => { let (place, ty) = self.translate_place_with_type(span, place)?; if let TyKind::Adt(TypeId::Adt(adt_id), _) = ty.kind() { @@ -1362,6 +1363,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { hax::FullDefKind::Closure { args, .. } => &args.sig, hax::FullDefKind::Fn { sig, .. } => sig, hax::FullDefKind::AssocFn { sig, .. } => sig, + hax::FullDefKind::Ctor { .. } => { + error_or_panic!( + self, + span, + "Casting constructors to function pointers is not supported" + ) + } _ => panic!("Unexpected definition for function: {def:?}"), }; diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index 456b8137..8ecaebac 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -241,7 +241,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // the type information in the const generic parameters // directly? For now we just ignore it. } - ClauseKind::WellFormed(_) | ClauseKind::ConstEvaluatable(_) => { + ClauseKind::WellFormed(_) => { + error_or_panic!( + ctx, + span, + format!("Well-formedness clauses are unsupported") + ) + } + ClauseKind::ConstEvaluatable(_) => { error_or_panic!(ctx, span, format!("Unsupported clause: {:?}", kind)) } } diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 575cb0cf..9bd7565a 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -178,7 +178,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { return self.translate_ty(span, erase_regions, hidden_ty) } _ => { - error_or_panic!(self, span, format!("Unimplemented: {:?}", ty)) + error_or_panic!( + self, + span, + format!("Unsupported alias type: {:?}", alias.kind) + ) } }, diff --git a/charon/src/transform/hide_marker_traits.rs b/charon/src/transform/hide_marker_traits.rs index 83a822f7..fa3c7e40 100644 --- a/charon/src/transform/hide_marker_traits.rs +++ b/charon/src/transform/hide_marker_traits.rs @@ -94,7 +94,8 @@ impl TransformPass for Transform { .item_names .iter() .filter(|(_, name)| exclude.iter().any(|p| p.matches(&ctx.translated, name))) - .map(|(id, _)| *id.as_trait_decl().unwrap()) + .filter_map(|(id, _)| id.as_trait_decl()) + .copied() .collect(); for &id in &exclude { diff --git a/charon/tests/ui/error-dependencies.rs b/charon/tests/ui/error-dependencies.rs index b0ab6aa8..e573af17 100644 --- a/charon/tests/ui/error-dependencies.rs +++ b/charon/tests/ui/error-dependencies.rs @@ -1,5 +1,5 @@ //@ known-failure -//! This file tests the error messages that indicates why we attempte to translate a given +//! This file tests the error messages that indicates why we attempt to translate a given //! definition. #![feature(register_tool)] #![register_tool(charon)] diff --git a/charon/tests/ui/issue-378-ctor-as-fn.out b/charon/tests/ui/issue-378-ctor-as-fn.out index 483f4935..13e09ad4 100644 --- a/charon/tests/ui/issue-378-ctor-as-fn.out +++ b/charon/tests/ui/issue-378-ctor-as-fn.out @@ -1,6 +1,18 @@ -error: Unexpected DefPathData for `core::option::Option::Some::{constructor#0}`: DisambiguatedDefPathData { data: Ctor, disambiguator: 0 } +error: Casting constructors to function pointers is not supported --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:579:5 -error: aborting due to 1 previous error +error: Ignoring the following item due to an error: core::option::Option::Some::{constructor#0} + --> /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/library/core/src/option.rs:579:5 + +error: The external definition `core::option::Option::Some` triggered errors. It is (transitively) used at the following location(s): + --> tests/ui/issue-378-ctor-as-fn.rs:3:34 + | +3 | static F: fn(u8) -> Option = Some; + | ^^^^ +... +6 | let f: fn(u8) -> _ = Some; + | ^^^^ + +error: aborting due to 3 previous errors Error: Charon driver exited with code 101 diff --git a/charon/tests/ui/unsupported/unbound-lifetime.out b/charon/tests/ui/unsupported/unbound-lifetime.out index c412b5f3..881685ef 100644 --- a/charon/tests/ui/unsupported/unbound-lifetime.out +++ b/charon/tests/ui/unsupported/unbound-lifetime.out @@ -1,7 +1,7 @@ error[E0261]: use of undeclared lifetime name `'a` - --> tests/ui/unsupported/unbound-lifetime.rs:4:13 + --> tests/ui/unsupported/unbound-lifetime.rs:5:13 | -4 | fn get(_x: &'a u32) {} +5 | fn get(_x: &'a u32) {} | - ^^ undeclared lifetime | | | help: consider introducing lifetime `'a` here: `<'a>` @@ -13,15 +13,15 @@ error: Could not find region: Region { kind: ReError(ErrorGuaranteed { todo: "Er Bound region vars: [[]] - --> tests/ui/unsupported/unbound-lifetime.rs:4:1 + --> tests/ui/unsupported/unbound-lifetime.rs:5:1 | -4 | fn get(_x: &'a u32) {} +5 | fn get(_x: &'a u32) {} | ^^^^^^^^^^^^^^^^^^^^^^ error: Ignoring the following item due to an error: test_crate::get - --> tests/ui/unsupported/unbound-lifetime.rs:4:1 + --> tests/ui/unsupported/unbound-lifetime.rs:5:1 | -4 | fn get(_x: &'a u32) {} +5 | fn get(_x: &'a u32) {} | ^^^^^^^^^^^^^^^^^^^ error: aborting due to 3 previous errors diff --git a/charon/tests/ui/unsupported/unbound-lifetime.rs b/charon/tests/ui/unsupported/unbound-lifetime.rs index db498815..466bb46d 100644 --- a/charon/tests/ui/unsupported/unbound-lifetime.rs +++ b/charon/tests/ui/unsupported/unbound-lifetime.rs @@ -1,4 +1,5 @@ //@ known-failure +// See https://github.com/AeneasVerif/charon/issues/306 // This is incorrect code but the error is weird. fn get(_x: &'a u32) {} diff --git a/charon/tests/ui/unsupported/well-formedness-bound.out b/charon/tests/ui/unsupported/well-formedness-bound.out index f576b183..bc782121 100644 --- a/charon/tests/ui/unsupported/well-formedness-bound.out +++ b/charon/tests/ui/unsupported/well-formedness-bound.out @@ -1,4 +1,4 @@ -error: Unsupported clause: WellFormed(Type(Ty { kind: Ref(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) }, Ty { kind: Tuple([]) }, false) })) +error: Well-formedness clauses are unsupported --> tests/ui/unsupported/well-formedness-bound.rs:4:5 | 4 | &'a ():,