miri: make NaN generation non-deterministic
This commit is contained in:
parent
d087c6fae2
commit
6796c5765d
6 changed files with 385 additions and 25 deletions
|
@ -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;
|
||||
use rustc_ast::{InlineAsmOptions, InlineAsmTemplatePiece};
|
||||
use rustc_middle::mir;
|
||||
use rustc_middle::ty::layout::TyAndLayout;
|
||||
|
@ -240,6 +241,13 @@ 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<F: Float>(_ecx: &InterpCx<'mir, 'tcx, Self>, _inputs: &[F]) -> F {
|
||||
// By default we always return the preferred NaN.
|
||||
F::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.
|
||||
|
|
|
@ -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)
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue