Auto merge of #116551 - RalfJung:nondet-nan, r=oli-obk
miri: make NaN generation non-deterministic This implements the [LLVM semantics for NaN generation](https://llvm.org/docs/LangRef.html#behavior-of-floating-point-nan-values). I will soon submit an RFC to make this also officially the Rust semantics, but it has been our de-facto semantics for a long time so there's no reason Miri has to wait for that RFC. This PR just better aligns Miri with codegen. This PR does that just for the operations that have MIR primitives; a future PR will adjust the intrinsics.
This commit is contained in:
commit
061c33051a
7 changed files with 531 additions and 29 deletions
|
@ -311,6 +311,21 @@ impl<'mir, 'tcx: 'mir, M: Machine<'mir, 'tcx>> InterpCx<'mir, 'tcx, M> {
|
|||
F: Float + Into<Scalar<M::Provenance>> + FloatConvert<Single> + FloatConvert<Double>,
|
||||
{
|
||||
use rustc_type_ir::sty::TyKind::*;
|
||||
|
||||
fn adjust_nan<
|
||||
'mir,
|
||||
'tcx: 'mir,
|
||||
M: Machine<'mir, 'tcx>,
|
||||
F1: rustc_apfloat::Float + FloatConvert<F2>,
|
||||
F2: rustc_apfloat::Float,
|
||||
>(
|
||||
ecx: &InterpCx<'mir, 'tcx, M>,
|
||||
f1: F1,
|
||||
f2: F2,
|
||||
) -> F2 {
|
||||
if f2.is_nan() { M::generate_nan(ecx, &[f1]) } else { f2 }
|
||||
}
|
||||
|
||||
match *dest_ty.kind() {
|
||||
// float -> uint
|
||||
Uint(t) => {
|
||||
|
@ -330,9 +345,13 @@ impl<'mir, 'tcx: 'mir, M: Machine<'mir, 'tcx>> InterpCx<'mir, 'tcx, M> {
|
|||
Scalar::from_int(v, size)
|
||||
}
|
||||
// float -> f32
|
||||
Float(FloatTy::F32) => Scalar::from_f32(f.convert(&mut false).value),
|
||||
Float(FloatTy::F32) => {
|
||||
Scalar::from_f32(adjust_nan(self, f, f.convert(&mut false).value))
|
||||
}
|
||||
// float -> f64
|
||||
Float(FloatTy::F64) => Scalar::from_f64(f.convert(&mut false).value),
|
||||
Float(FloatTy::F64) => {
|
||||
Scalar::from_f64(adjust_nan(self, f, f.convert(&mut false).value))
|
||||
}
|
||||
// That's it.
|
||||
_ => span_bug!(self.cur_span(), "invalid float to {} cast", dest_ty),
|
||||
}
|
||||
|
|
|
@ -500,6 +500,9 @@ impl<'mir, 'tcx: 'mir, M: Machine<'mir, 'tcx>> InterpCx<'mir, 'tcx, M> {
|
|||
b: &ImmTy<'tcx, M::Provenance>,
|
||||
dest: &PlaceTy<'tcx, M::Provenance>,
|
||||
) -> InterpResult<'tcx> {
|
||||
assert_eq!(a.layout.ty, b.layout.ty);
|
||||
assert!(matches!(a.layout.ty.kind(), ty::Int(..) | ty::Uint(..)));
|
||||
|
||||
// Performs an exact division, resulting in undefined behavior where
|
||||
// `x % y != 0` or `y == 0` or `x == T::MIN && y == -1`.
|
||||
// First, check x % y != 0 (or if that computation overflows).
|
||||
|
@ -522,7 +525,10 @@ impl<'mir, 'tcx: 'mir, M: Machine<'mir, 'tcx>> InterpCx<'mir, 'tcx, M> {
|
|||
l: &ImmTy<'tcx, M::Provenance>,
|
||||
r: &ImmTy<'tcx, M::Provenance>,
|
||||
) -> InterpResult<'tcx, Scalar<M::Provenance>> {
|
||||
assert_eq!(l.layout.ty, r.layout.ty);
|
||||
assert!(matches!(l.layout.ty.kind(), ty::Int(..) | ty::Uint(..)));
|
||||
assert!(matches!(mir_op, BinOp::Add | BinOp::Sub));
|
||||
|
||||
let (val, overflowed) = self.overflowing_binary_op(mir_op, l, r)?;
|
||||
Ok(if overflowed {
|
||||
let size = l.layout.size;
|
||||
|
|
|
@ -6,6 +6,7 @@ use std::borrow::{Borrow, Cow};
|
|||
use std::fmt::Debug;
|
||||
use std::hash::Hash;
|
||||
|
||||
use rustc_apfloat::{Float, FloatConvert};
|
||||
use rustc_ast::{InlineAsmOptions, InlineAsmTemplatePiece};
|
||||
use rustc_middle::mir;
|
||||
use rustc_middle::ty::layout::TyAndLayout;
|
||||
|
@ -240,6 +241,16 @@ pub trait Machine<'mir, 'tcx: 'mir>: Sized {
|
|||
right: &ImmTy<'tcx, Self::Provenance>,
|
||||
) -> InterpResult<'tcx, (ImmTy<'tcx, Self::Provenance>, bool)>;
|
||||
|
||||
/// Generate the NaN returned by a float operation, given the list of inputs.
|
||||
/// (This is all inputs, not just NaN inputs!)
|
||||
fn generate_nan<F1: Float + FloatConvert<F2>, F2: Float>(
|
||||
_ecx: &InterpCx<'mir, 'tcx, Self>,
|
||||
_inputs: &[F1],
|
||||
) -> F2 {
|
||||
// By default we always return the preferred NaN.
|
||||
F2::NAN
|
||||
}
|
||||
|
||||
/// Called before writing the specified `local` of the `frame`.
|
||||
/// Since writing a ZST is not actually accessing memory or locals, this is never invoked
|
||||
/// for ZST reads.
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
use rustc_apfloat::Float;
|
||||
use rustc_apfloat::{Float, FloatConvert};
|
||||
use rustc_middle::mir;
|
||||
use rustc_middle::mir::interpret::{InterpResult, Scalar};
|
||||
use rustc_middle::ty::layout::TyAndLayout;
|
||||
|
@ -104,7 +104,7 @@ impl<'mir, 'tcx: 'mir, M: Machine<'mir, 'tcx>> InterpCx<'mir, 'tcx, M> {
|
|||
(ImmTy::from_bool(res, *self.tcx), false)
|
||||
}
|
||||
|
||||
fn binary_float_op<F: Float + Into<Scalar<M::Provenance>>>(
|
||||
fn binary_float_op<F: Float + FloatConvert<F> + Into<Scalar<M::Provenance>>>(
|
||||
&self,
|
||||
bin_op: mir::BinOp,
|
||||
layout: TyAndLayout<'tcx>,
|
||||
|
@ -113,6 +113,11 @@ impl<'mir, 'tcx: 'mir, M: Machine<'mir, 'tcx>> InterpCx<'mir, 'tcx, M> {
|
|||
) -> (ImmTy<'tcx, M::Provenance>, bool) {
|
||||
use rustc_middle::mir::BinOp::*;
|
||||
|
||||
// Performs appropriate non-deterministic adjustments of NaN results.
|
||||
let adjust_nan = |f: F| -> F {
|
||||
if f.is_nan() { M::generate_nan(self, &[l, r]) } else { f }
|
||||
};
|
||||
|
||||
let val = match bin_op {
|
||||
Eq => ImmTy::from_bool(l == r, *self.tcx),
|
||||
Ne => ImmTy::from_bool(l != r, *self.tcx),
|
||||
|
@ -120,11 +125,11 @@ impl<'mir, 'tcx: 'mir, M: Machine<'mir, 'tcx>> InterpCx<'mir, 'tcx, M> {
|
|||
Le => ImmTy::from_bool(l <= r, *self.tcx),
|
||||
Gt => ImmTy::from_bool(l > r, *self.tcx),
|
||||
Ge => ImmTy::from_bool(l >= r, *self.tcx),
|
||||
Add => ImmTy::from_scalar((l + r).value.into(), layout),
|
||||
Sub => ImmTy::from_scalar((l - r).value.into(), layout),
|
||||
Mul => ImmTy::from_scalar((l * r).value.into(), layout),
|
||||
Div => ImmTy::from_scalar((l / r).value.into(), layout),
|
||||
Rem => ImmTy::from_scalar((l % r).value.into(), layout),
|
||||
Add => ImmTy::from_scalar(adjust_nan((l + r).value).into(), layout),
|
||||
Sub => ImmTy::from_scalar(adjust_nan((l - r).value).into(), layout),
|
||||
Mul => ImmTy::from_scalar(adjust_nan((l * r).value).into(), layout),
|
||||
Div => ImmTy::from_scalar(adjust_nan((l / r).value).into(), layout),
|
||||
Rem => ImmTy::from_scalar(adjust_nan((l % r).value).into(), layout),
|
||||
_ => span_bug!(self.cur_span(), "invalid float op: `{:?}`", bin_op),
|
||||
};
|
||||
(val, false)
|
||||
|
@ -456,6 +461,7 @@ impl<'mir, 'tcx: 'mir, M: Machine<'mir, 'tcx>> InterpCx<'mir, 'tcx, M> {
|
|||
Ok((ImmTy::from_bool(res, *self.tcx), false))
|
||||
}
|
||||
ty::Float(fty) => {
|
||||
// No NaN adjustment here, `-` is a bitwise operation!
|
||||
let res = match (un_op, fty) {
|
||||
(Neg, FloatTy::F32) => Scalar::from_f32(-val.to_f32()?),
|
||||
(Neg, FloatTy::F64) => Scalar::from_f64(-val.to_f64()?),
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue