Merge pull request #1015 from creusot-rs/better-errors

Slightly better error messages

creusot/src/backend/program.rs

@@ -314,6 +314,7 @@ impl<'tcx> RValue<'tcx> {
         ctx: &mut Why3Generator<'tcx>,
         names: &mut N,
         locals: &LocalDecls<'tcx>,
+        span: Span,
         ty: Ty<'tcx>,
     ) -> Exp {
         let e = match self {
@@ -334,10 +335,10 @@ impl<'tcx> RValue<'tcx> {
             RValue::BinOp(op, l, r) => {
                 let ty = l.ty(ctx.tcx, locals);
                 // Hack
-                translate_ty(ctx, names, DUMMY_SP, ty);
+                translate_ty(ctx, names, span, ty);
 
                 Exp::BinaryOp(
-                    binop_to_binop(ctx, ty, op),
+                    binop_to_binop(ctx, span, ty, op),
                     Box::new(l.to_why(ctx, names, locals)),
                     Box::new(r.to_why(ctx, names, locals)),
                 )
@@ -369,8 +370,7 @@ impl<'tcx> RValue<'tcx> {
                         names.import_prelude_module(PreludeModule::Bool);
                         Exp::qvar(QName::from_string("Bool.to_int").unwrap())
                     }
-                    _ => ctx
-                        .crash_and_error(DUMMY_SP, "Non integral casts are currently unsupported"),
+                    _ => ctx.crash_and_error(span, "Non integral casts are currently unsupported"),
                 };
 
                 let from_int = match target.kind() {
@@ -380,8 +380,7 @@ impl<'tcx> RValue<'tcx> {
                         names.import_prelude_module(PreludeModule::Char);
                         Exp::qvar(QName::from_string("Char.chr").unwrap())
                     }
-                    _ => ctx
-                        .crash_and_error(DUMMY_SP, "Non integral casts are currently unsupported"),
+                    _ => ctx.crash_and_error(span, "Non integral casts are currently unsupported"),
                 };
 
                 from_int.app_to(to_int.app_to(e.to_why(ctx, names, locals)))
@@ -393,7 +392,7 @@ impl<'tcx> RValue<'tcx> {
             }
             RValue::Array(fields) => {
                 let id = Ident::build("__arr_temp");
-                let ty = translate_ty(ctx, names, DUMMY_SP, ty);
+                let ty = translate_ty(ctx, names, span, ty);
 
                 let len = fields.len();
 
@@ -706,7 +705,7 @@ impl<'tcx> Statement<'tcx> {
             Statement::Assignment(lhs, rhs, span) => {
                 let mut invalid = Vec::new();
                 rhs.invalidated_places(&mut invalid);
-                let rhs = rhs.to_why(ctx, names, locals, lhs.ty(ctx.tcx, locals));
+                let rhs = rhs.to_why(ctx, names, locals, span, lhs.ty(ctx.tcx, locals));
                 let mut exps =
                     vec![place::create_assign_inner(ctx, names, locals, &lhs, rhs, span)];
                 invalidate_places(ctx, names, locals, span, invalid, &mut exps);

creusot/src/ctx.rs

@@ -408,7 +408,10 @@ pub(crate) fn load_extern_specs(ctx: &mut TranslationCtx) -> CreusotResult<()> {
             let c = es.contract.clone();
 
             if ctx.extern_spec(i).is_some() {
-                ctx.crash_and_error(DUMMY_SP, &format!("duplicate extern specification for {i:?}"));
+                ctx.crash_and_error(
+                    ctx.def_span(def_id),
+                    &format!("duplicate extern specification for {i:?}"),
+                );
             };
 
             let _ = ctx.extern_specs.insert(i, es);

creusot/src/translation.rs

@@ -20,6 +20,7 @@ use ctx::TranslationCtx;
 use heck::ToUpperCamelCase;
 use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE};
 use rustc_middle::ty::Ty;
+use rustc_span::Span;
 use std::{error::Error, io::Write};
 use why3::{declaration::Module, mlcfg, Print};
 
@@ -126,7 +127,12 @@ pub(crate) fn after_analysis(ctx: TranslationCtx) -> Result<(), Box<dyn Error>>
 }
 use rustc_middle::mir;
 
-pub(crate) fn binop_to_binop(ctx: &mut TranslationCtx, ty: Ty, op: mir::BinOp) -> why3::exp::BinOp {
+pub(crate) fn binop_to_binop(
+    ctx: &mut TranslationCtx,
+    span: Span,
+    ty: Ty,
+    op: mir::BinOp,
+) -> why3::exp::BinOp {
     use why3::exp::BinOp;
     match op {
         mir::BinOp::Add => {
@@ -194,10 +200,7 @@ pub(crate) fn binop_to_binop(ctx: &mut TranslationCtx, ty: Ty, op: mir::BinOp) -
         }
         mir::BinOp::Ne => BinOp::Ne,
         mir::BinOp::Rem => BinOp::Mod,
-        _ => ctx.crash_and_error(
-            rustc_span::DUMMY_SP,
-            &format!("unsupported binary operation: {:?}", op),
-        ),
+        _ => ctx.crash_and_error(span, &format!("unsupported binary operation: {:?}", op)),
     }
 }
 

creusot/src/translation/constant.rs

@@ -85,7 +85,7 @@ pub(crate) fn from_ty_const<'tcx>(
     return Term { kind: TermKind::Lit(try_to_bits(ctx, env, c.ty(), span, c)), ty: c.ty(), span };
 }
 
-fn try_to_bits<'tcx, C: ToBits<'tcx>>(
+fn try_to_bits<'tcx, C: ToBits<'tcx> + std::fmt::Debug>(
     ctx: &mut TranslationCtx<'tcx>,
     // names: &mut CloneMap<'tcx>,
     env: ParamEnv<'tcx>,
@@ -95,9 +95,11 @@ fn try_to_bits<'tcx, C: ToBits<'tcx>>(
 ) -> Literal<'tcx> {
     use rustc_middle::ty::{FloatTy, IntTy, UintTy};
     use rustc_type_ir::TyKind::{Bool, Float, FnDef, Int, Uint};
+    let Some(bits) = c.get_bits(ctx.tcx, env, ty) else {
+        ctx.fatal_error(span, &format!("Could determine value of constant. Creusot currently does not support generic associated constants.")).emit()
+    };
     match ty.kind() {
         Int(ity) => {
-            let bits = c.get_bits(ctx.tcx, env, ty).unwrap();
             let bits: i128 = match *ity {
                 IntTy::I128 => bits as i128,
                 IntTy::Isize => bits as i64 as i128,
@@ -109,7 +111,6 @@ fn try_to_bits<'tcx, C: ToBits<'tcx>>(
             Literal::MachSigned(bits, *ity)
         }
         Uint(uty) => {
-            let bits = c.get_bits(ctx.tcx, env, ty).unwrap();
             let bits: u128 = match *uty {
                 UintTy::U128 => bits as u128,
                 UintTy::Usize => bits as u64 as u128,
@@ -120,19 +121,17 @@ fn try_to_bits<'tcx, C: ToBits<'tcx>>(
             };
             Literal::MachUnsigned(bits, *uty)
         }
-        Bool => Literal::Bool(c.get_bits(ctx.tcx, env, ty) == Some(1)),
+        Bool => Literal::Bool(bits == 1),
         Float(FloatTy::F32) => {
-            let bits = c.get_bits(ctx.tcx, env, ty);
-            let float = f32::from_bits(bits.unwrap() as u32);
+            let float = f32::from_bits(bits as u32);
             if float.is_nan() {
                 ctx.crash_and_error(span, "NaN is not yet supported")
             } else {
                 Literal::Float((float as f64).into(), FloatTy::F32)
             }
         }
         Float(FloatTy::F64) => {
-            let bits = c.get_bits(ctx.tcx, env, ty);
-            let float = f64::from_bits(bits.unwrap() as u64);
+            let float = f64::from_bits(bits as u64);
             if float.is_nan() {
                 ctx.crash_and_error(span, "NaN is not yet supported")
             } else {

creusot/src/translation/pearlite.rs

@@ -334,19 +334,34 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                     mir::BinOp::Div => BinOp::Div,
                     mir::BinOp::Rem => BinOp::Rem,
                     mir::BinOp::BitXor => {
-                        return Err(Error::new(self.thir[expr].span, "unsupported operation"))
+                        return Err(Error::new(
+                            self.thir[expr].span,
+                            "bitwise-xors are currently unsupported",
+                        ))
                     }
                     mir::BinOp::BitAnd => {
-                        return Err(Error::new(self.thir[expr].span, "unsupported operation"))
+                        return Err(Error::new(
+                            self.thir[expr].span,
+                            "bitwise-ands are currently unsupported",
+                        ))
                     }
                     mir::BinOp::BitOr => {
-                        return Err(Error::new(self.thir[expr].span, "unsupported operation"))
+                        return Err(Error::new(
+                            self.thir[expr].span,
+                            "bitwise-ors are currently unsupported",
+                        ))
                     }
                     mir::BinOp::Shl | mir::BinOp::ShlUnchecked => {
-                        return Err(Error::new(self.thir[expr].span, "unsupported operation"))
+                        return Err(Error::new(
+                            self.thir[expr].span,
+                            "shifts are currently unsupported",
+                        ))
                     }
                     mir::BinOp::Shr | mir::BinOp::ShrUnchecked => {
-                        return Err(Error::new(self.thir[expr].span, "unsupported operation"))
+                        return Err(Error::new(
+                            self.thir[expr].span,
+                            "shifts are currently unsupported",
+                        ))
                     }
                     mir::BinOp::Lt => BinOp::Lt,
                     mir::BinOp::Le => BinOp::Le,