Improve some error messages

AeneasVerif · Oct 16, 2024 · a1566c0 · a1566c0
1 parent 5818d1e
commit a1566c0
Show file tree

Hide file tree

Showing 10 changed files with 63 additions and 25 deletions.
diff --git 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
@@ -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<BinOp, Error> {
         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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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<u8> = 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
@@ -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
@@ -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
@@ -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 ():,