Merge pull request #422 from Nadrieril/improve-errors

AeneasVerif · Oct 16, 2024 · 53a3af4 · 53a3af4
2 parents b1ed995 + a1566c0
commit 53a3af4
Show file tree

Hide file tree

Showing 25 changed files with 485 additions and 188 deletions.
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs
@@ -34,6 +34,7 @@ use crate::driver::{
 use charon_lib::logger;
 use charon_lib::options;
 use charon_lib::trace;
+use itertools::Itertools;
 
 fn main() {
     // Initialize the logger
@@ -191,6 +192,52 @@ fn main() {
         compiler_args.push(extra_flag);
     }
 
+    let disabled_mir_passes = [
+        "AfterConstProp",
+        "AfterGVN",
+        "AfterUnreachableEnumBranching)",
+        "BeforeConstProp",
+        "CheckAlignment",
+        "CopyProp",
+        "CriticalCallEdges",
+        "DataflowConstProp",
+        "DeduplicateBlocks",
+        "DestinationPropagation",
+        "EarlyOtherwiseBranch",
+        "EnumSizeOpt",
+        "GVN",
+        "Initial",
+        "Inline",
+        "InstSimplify",
+        "JumpThreading",
+        "LowerSliceLenCalls",
+        "MatchBranchSimplification",
+        "MentionedItems",
+        "MultipleReturnTerminators",
+        "ReferencePropagation",
+        "RemoveNoopLandingPads",
+        "RemoveStorageMarkers",
+        "RemoveUnneededDrops",
+        "RemoveZsts",
+        "RenameReturnPlace",
+        "ReorderBasicBlocks",
+        "ReorderLocals",
+        "ScalarReplacementOfAggregates",
+        "SimplifyComparisonIntegral",
+        "SimplifyLocals",
+        "SingleUseConsts",
+        "UnreachableEnumBranching",
+        "UnreachablePropagation",
+    ];
+    // Disable all these mir passes.
+    compiler_args.push(format!(
+        "-Zmir-enable-passes={}",
+        disabled_mir_passes
+            .iter()
+            .map(|p| format!("-{p}"))
+            .format(",")
+    ));
+
     trace!("Compiler arguments: {:?}", compiler_args);
 
     // Call the Rust compiler with our custom callback.

diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs
@@ -111,9 +111,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             }
             ConstantExprKind::TraitConst { impl_expr, name } => {
                 let trait_ref = self.translate_trait_impl_expr(span, erase_regions, impl_expr)?;
-                // The trait ref should be Some(...): trait markers (that we
-                // may eliminate) don't have constants.
-                let trait_ref = trait_ref.unwrap();
                 let name = TraitItemName(name.clone());
                 RawConstantExpr::TraitConst(trait_ref, name)
             }

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() {
@@ -848,18 +849,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             let fun_id = self.register_fun_decl_id(span, def_id);
             // Two cases depending on whether we call a trait method or not
             match trait_info {
-                None => {
-                    // "Regular" function call
-                    FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id))
-                }
+                // Direct function call
+                None => FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)),
+                // Trait method
                 Some(trait_info) => {
-                    // Trait method
                     let impl_expr =
                         self.translate_trait_impl_expr(span, erase_regions, trait_info)?;
-                    // The impl source should be Some(...): trait markers (that we may
-                    // eliminate) don't have methods.
-                    let impl_expr = impl_expr.unwrap();
-
                     let method_name = self.t_ctx.translate_trait_item_name(def_id)?;
                     FunIdOrTraitMethodRef::Trait(impl_expr, method_name, fun_id)
                 }
@@ -1368,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
@@ -1,7 +1,9 @@
 use super::translate_ctx::*;
 use super::translate_traits::PredicateLocation;
 use charon_lib::ast::*;
+use charon_lib::formatter::IntoFormatter;
 use charon_lib::ids::Vector;
+use charon_lib::pretty::FmtWithCtx;
 use hax_frontend_exporter as hax;
 
 impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
@@ -79,14 +81,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         Ok(())
     }
 
-    /// Returns an [Option] because we may filter trait refs about builtin or
-    /// auto traits like [core::marker::Sized] and [core::marker::Sync].
     pub(crate) fn translate_trait_decl_ref(
         &mut self,
         span: Span,
         erase_regions: bool,
         bound_trait_ref: &hax::Binder<hax::TraitRef>,
-    ) -> Result<Option<PolyTraitDeclRef>, Error> {
+    ) -> Result<PolyTraitDeclRef, Error> {
         let binder = bound_trait_ref.rebind(());
         self.with_locally_bound_regions_group(span, binder, move |ctx| {
             let trait_ref = bound_trait_ref.hax_skip_binder_ref();
@@ -100,10 +100,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 &parent_trait_refs,
             )?;
 
-            Ok(Some(RegionBinder {
+            Ok(RegionBinder {
                 regions: ctx.region_vars[0].clone(),
                 skip_binder: TraitDeclRef { trait_id, generics },
-            }))
+            })
         })
     }
 
@@ -223,10 +223,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                             let trait_ref =
                                 ctx.translate_trait_impl_expr(span, erase_regions, impl_expr)?;
-                            // The trait ref should be Some(...): the marker traits (that
-                            // we may filter) don't have associated types.
-                            let trait_ref = trait_ref.unwrap();
-                            let ty = ctx.translate_ty(span, erase_regions, ty).unwrap();
+                            let ty = ctx.translate_ty(span, erase_regions, ty)?;
                             let type_name = TraitItemName(assoc_item.name.clone().into());
                             ctx.generic_params
                                 .trait_type_constraints
@@ -244,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))
                         }
                     }
@@ -270,27 +274,21 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         erase_regions: bool,
         impl_sources: &[hax::ImplExpr],
     ) -> Result<Vector<TraitClauseId, TraitRef>, Error> {
-        let res: Vec<_> = impl_sources
+        impl_sources
             .iter()
             .map(|x| self.translate_trait_impl_expr(span, erase_regions, x))
-            .try_collect()?;
-        Ok(res.into_iter().flatten().collect())
+            .try_collect()
     }
 
-    /// Returns an [Option] because we may ignore some builtin or auto traits
-    /// like [core::marker::Sized] or [core::marker::Sync].
     #[tracing::instrument(skip(self, span, erase_regions, impl_expr))]
     pub(crate) fn translate_trait_impl_expr(
         &mut self,
         span: Span,
         erase_regions: bool,
         impl_expr: &hax::ImplExpr,
-    ) -> Result<Option<TraitRef>, Error> {
+    ) -> Result<TraitRef, Error> {
         let trait_decl_ref =
-            match self.translate_trait_decl_ref(span, erase_regions, &impl_expr.r#trait)? {
-                None => return Ok(None),
-                Some(tr) => tr,
-            };
+            self.translate_trait_decl_ref(span, erase_regions, &impl_expr.r#trait)?;
 
         match self.translate_trait_impl_expr_aux(
             span,
@@ -305,10 +303,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 } else {
                     let msg = format!("Error during trait resolution: {}", &err.msg);
                     self.span_err(span, &msg);
-                    Ok(Some(TraitRef {
+                    Ok(TraitRef {
                         kind: TraitRefKind::Unknown(err.msg),
                         trait_decl_ref,
-                    }))
+                    })
                 }
             }
         }
@@ -320,7 +318,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         erase_regions: bool,
         impl_source: &hax::ImplExpr,
         trait_decl_ref: PolyTraitDeclRef,
-    ) -> Result<Option<TraitRef>, Error> {
+    ) -> Result<TraitRef, Error> {
         trace!("impl_expr: {:#?}", impl_source);
         use hax::ImplExprAtom;
 
@@ -378,10 +376,22 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     match path_elem {
                         AssocItem {
                             item,
+                            generic_args,
                             predicate,
                             index,
-                            predicate_id: _,
+                            ..
                         } => {
+                            if !generic_args.is_empty() {
+                                error_or_panic!(
+                                    self,
+                                    span,
+                                    format!(
+                                        "Found unsupported GAT `{}` when resolving trait `{}`",
+                                        item.name,
+                                        trait_decl_ref.fmt_with_ctx(&self.into_fmt())
+                                    )
+                                )
+                            }
                             trait_id = TraitRefKind::ItemClause(
                                 Box::new(trait_id),
                                 current_trait_decl_id,
@@ -394,9 +404,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                             );
                         }
                         Parent {
-                            predicate,
-                            index,
-                            predicate_id: _,
+                            predicate, index, ..
                         } => {
                             trait_id = TraitRefKind::ParentClause(
                                 Box::new(trait_id),
@@ -441,6 +449,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 trait_ref
             }
         };
-        Ok(Some(trait_ref))
+        Ok(trait_ref)
     }
 }