diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs index 638a78cae4..140bfa6b80 100644 --- a/creusot/src/backend/program.rs +++ b/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); diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs index 175254a55d..a8923c236c 100644 --- a/creusot/src/ctx.rs +++ b/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); diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs index db607cc7f0..0f6dcc7e71 100644 --- a/creusot/src/translation.rs +++ b/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> } 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)), } } diff --git a/creusot/src/translation/constant.rs b/creusot/src/translation/constant.rs index 4523478c04..da1cc19aa9 100644 --- a/creusot/src/translation/constant.rs +++ b/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,10 +121,9 @@ 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 { @@ -131,8 +131,7 @@ fn try_to_bits<'tcx, C: ToBits<'tcx>>( } } 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 { diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs index 4d5dee2385..0d6b936dda 100644 --- a/creusot/src/translation/pearlite.rs +++ b/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,