Skip to content

Latest commit

 

History

History
140 lines (114 loc) · 6.67 KB

0014-convert-num.md

File metadata and controls

140 lines (114 loc) · 6.67 KB

Challenge 14: Safety of Primitive Conversions

  • Status: Open
  • Tracking Issue: model-checking#220
  • Start date: 2024/12/15
  • End date: 2025/2/28
  • Prize: TBD

Goal

Verify the safety of number conversions in core::convert::num.

There are three classes of conversions that use unsafe code. All conversions use macros to implement traits for primitive types in bulk. You will need to add contracts into the macros so that contracts are generated for each implementation. As the conversions are all macro generated, it is probably a good idea to write your own macro for generating the harnesses.

Success Criteria

Safety for Float to Int

macro_rules! impl_float_to_int {
    ($Float:ty => $($Int:ty),+) => {
        #[unstable(feature = "convert_float_to_int", issue = "67057")]
        impl private::Sealed for $Float {}
        $(
            #[unstable(feature = "convert_float_to_int", issue = "67057")]
            impl FloatToInt<$Int> for $Float {
                #[inline]
                unsafe fn to_int_unchecked(self) -> $Int {
                    // SAFETY: the safety contract must be upheld by the caller.
                    unsafe { crate::intrinsics::float_to_int_unchecked(self) }
                }
            }
        )+
    }
}

The safety constraints referenced in the comments are that the input value must:

  • Not be NaN
  • Not be infinite
  • Be representable in the return type Int, after truncating off its fractional part

These constraints are given in the documenation.

The intrinsic corresponds to the fptoui/fptosi LLVM instructions, which may be useful for reference.

NonZero Conversions

Write a type invariant for core::num::NonZero, then write harnesses for all nonzero conversions.

There are two macros that implement these conversions: an infallible and fallible version. These are all of the types for which conversions are implemented. You should be able to use the macro to generate the function contracts.

non-zero unsigned integer -> non-zero unsigned integer

  • impl_nonzero_int_from_nonzero_int!(u8 => u16);
  • impl_nonzero_int_from_nonzero_int!(u8 => u32);
  • impl_nonzero_int_from_nonzero_int!(u8 => u64);
  • impl_nonzero_int_from_nonzero_int!(u8 => u128);
  • impl_nonzero_int_from_nonzero_int!(u8 => usize);
  • impl_nonzero_int_from_nonzero_int!(u16 => u32);
  • impl_nonzero_int_from_nonzero_int!(u16 => u64);
  • impl_nonzero_int_from_nonzero_int!(u16 => u128);
  • impl_nonzero_int_from_nonzero_int!(u16 => usize);
  • impl_nonzero_int_from_nonzero_int!(u32 => u64);
  • impl_nonzero_int_from_nonzero_int!(u32 => u128);
  • impl_nonzero_int_from_nonzero_int!(u64 => u128);

non-zero signed integer -> non-zero signed integer

  • impl_nonzero_int_from_nonzero_int!(i8 => i16);
  • impl_nonzero_int_from_nonzero_int!(i8 => i32);
  • impl_nonzero_int_from_nonzero_int!(i8 => i64);
  • impl_nonzero_int_from_nonzero_int!(i8 => i128);
  • impl_nonzero_int_from_nonzero_int!(i8 => isize);
  • impl_nonzero_int_from_nonzero_int!(i16 => i32);
  • impl_nonzero_int_from_nonzero_int!(i16 => i64);
  • impl_nonzero_int_from_nonzero_int!(i16 => i128);
  • impl_nonzero_int_from_nonzero_int!(i16 => isize);
  • impl_nonzero_int_from_nonzero_int!(i32 => i64);
  • impl_nonzero_int_from_nonzero_int!(i32 => i128);
  • impl_nonzero_int_from_nonzero_int!(i64 => i128);

non-zero unsigned -> non-zero signed integer

  • impl_nonzero_int_from_nonzero_int!(u8 => i16);
  • impl_nonzero_int_from_nonzero_int!(u8 => i32);
  • impl_nonzero_int_from_nonzero_int!(u8 => i64);
  • impl_nonzero_int_from_nonzero_int!(u8 => i128);
  • impl_nonzero_int_from_nonzero_int!(u8 => isize);
  • impl_nonzero_int_from_nonzero_int!(u16 => i32);
  • impl_nonzero_int_from_nonzero_int!(u16 => i64);
  • impl_nonzero_int_from_nonzero_int!(u16 => i128);
  • impl_nonzero_int_from_nonzero_int!(u32 => i64);
  • impl_nonzero_int_from_nonzero_int!(u32 => i128);
  • impl_nonzero_int_from_nonzero_int!(u64 => i128);

There are also the fallible versions.

unsigned non-zero integer -> unsigned non-zero integer

  • impl_nonzero_int_try_from_nonzero_int!(u16 => u8);
  • impl_nonzero_int_try_from_nonzero_int!(u32 => u8, u16, usize);
  • impl_nonzero_int_try_from_nonzero_int!(u64 => u8, u16, u32, usize);
  • impl_nonzero_int_try_from_nonzero_int!(u128 => u8, u16, u32, u64, usize);
  • impl_nonzero_int_try_from_nonzero_int!(usize => u8, u16, u32, u64, u128);

signed non-zero integer -> signed non-zero integer

  • impl_nonzero_int_try_from_nonzero_int!(i16 => i8);
  • impl_nonzero_int_try_from_nonzero_int!(i32 => i8, i16, isize);
  • impl_nonzero_int_try_from_nonzero_int!(i64 => i8, i16, i32, isize);
  • impl_nonzero_int_try_from_nonzero_int!(i128 => i8, i16, i32, i64, isize);
  • impl_nonzero_int_try_from_nonzero_int!(isize => i8, i16, i32, i64, i128);

unsigned non-zero integer -> signed non-zero integer

  • impl_nonzero_int_try_from_nonzero_int!(u8 => i8);
  • impl_nonzero_int_try_from_nonzero_int!(u16 => i8, i16, isize);
  • impl_nonzero_int_try_from_nonzero_int!(u32 => i8, i16, i32, isize);
  • impl_nonzero_int_try_from_nonzero_int!(u64 => i8, i16, i32, i64, isize);
  • impl_nonzero_int_try_from_nonzero_int!(u128 => i8, i16, i32, i64, i128, isize);
  • impl_nonzero_int_try_from_nonzero_int!(usize => i8, i16, i32, i64, i128, isize);

signed non-zero integer -> unsigned non-zero integer

  • impl_nonzero_int_try_from_nonzero_int!(i8 => u8, u16, u32, u64, u128, usize);
  • impl_nonzero_int_try_from_nonzero_int!(i16 => u8, u16, u32, u64, u128, usize);
  • impl_nonzero_int_try_from_nonzero_int!(i32 => u8, u16, u32, u64, u128, usize);
  • impl_nonzero_int_try_from_nonzero_int!(i64 => u8, u16, u32, u64, u128, usize);
  • impl_nonzero_int_try_from_nonzero_int!(i128 => u8, u16, u32, u64, u128, usize);
  • impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);

List of UBs

In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following undefined behaviors:

  • Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
  • Reading from uninitialized memory.
  • Mutating immutable bytes.
  • Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.