Skip to content

Commit 4beb481

Browse files
committed
Flesh out safety annotations
1 parent a44c70d commit 4beb481

File tree

8 files changed

+65
-19
lines changed

8 files changed

+65
-19
lines changed

src/posit/basics.rs

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -76,8 +76,13 @@ impl<
7676
Self(Self::sign_extend(bits))
7777
}
7878

79-
/// As [`Self::from_bits`], but if `bits` is not a result of a [`Self::to_bits`] call, then
80-
/// calling this function is undefined behaviour.
79+
/// As [`Self::from_bits`], but does not check that `bits` is a valid bit pattern for `Self`.
80+
///
81+
/// # Safety
82+
///
83+
/// `bits` has to be a result of a [`Self::to_bits`] call, i.e. it has to be in the range
84+
/// `-1 << (N-1) .. 1 << (N-1) - 1`, or calling this function is *undefined behaviour*. Note
85+
/// that if `Int::BITS == Self::BITS` this always holds.
8186
pub const unsafe fn from_bits_unchecked(bits: Int) -> Self {
8287
Self(bits)
8388
}
@@ -114,16 +119,19 @@ impl<
114119
/// and so on.
115120
pub(crate) const FRAC_DENOM: Int = const_as(1i128 << Self::FRAC_WIDTH);
116121

117-
/// The size of this Posit type in bits.
118-
///
119-
/// Note: this is the logical size, not necessarily the size of the underlying type.
122+
/// As [`Posit::BITS`].
120123
pub const BITS: u32 = Posit::<N, ES, Int>::BITS;
121124

122-
/// The number of exponent bits.
125+
/// As [`Posit::ES`].
123126
pub const ES: u32 = Posit::<N, ES, Int>::ES;
124127

125-
/// Checks whether `self` is normalised, i.e. whether `self.frac` starts with `0b01` or `0b10`,
126-
/// and `self.exp >> ES` starts with `0b00` or `0b11` (which is guaranteed if `ES > 0`).
128+
/// As [`Posit::JUNK_BITS`].
129+
pub(crate) const JUNK_BITS: u32 = Posit::<N, ES, Int>::ES;
130+
131+
/// Checks whether `self` is "normalised", i.e. whether
132+
///
133+
/// - `self.frac` starts with `0b01` or `0b10`, and
134+
/// - `self.exp >> ES` starts with `0b00` or `0b11` (which is guaranteed if `ES > 0`).
127135
pub(crate) fn is_normalised(self) -> bool {
128136
let frac = self.frac >> Self::FRAC_WIDTH;
129137
let exp = self.exp >> Self::FRAC_WIDTH;

src/posit/convert/int.rs

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,10 @@ use crate::underlying::const_as;
44

55
/// The kernel for converting a _signed_ int to a posit.
66
///
7-
/// If `int` is `FromInt::ZERO` or `FromInt::MIN`, calling this function is *undefined behaviour*.
7+
/// # Safety
8+
///
9+
/// `int` cannot be `FromInt::ZERO` or `FromInt::MIN`, or calling this function is *undefined
10+
/// behaviour*.
811
#[inline]
912
unsafe fn round_from_signed_kernel<
1013
FromInt: crate::Int,
@@ -54,7 +57,10 @@ unsafe fn round_from_signed_kernel<
5457
/// The kernel for converting an _unsigned_ int to a posit (note it takes a signed int as
5558
/// argument though).
5659
///
57-
/// If `int` is `FromInt::ZERO` or `FromInt::MIN`, calling this function is *undefined behaviour*.
60+
/// # Safety
61+
///
62+
/// `int` cannot be `FromInt::ZERO` or `FromInt::MIN`, or calling this function is *undefined
63+
/// behaviour*.
5864
#[inline]
5965
unsafe fn round_from_unsigned_kernel<
6066
FromInt: crate::Int,

src/posit/decode.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,10 @@ impl<
77
> Posit<N, ES, Int> {
88
/// Decode a posit **which is not 0 or NaR** into its constituent `frac`tion and `exp`onent.
99
///
10-
/// `self` cannot be 0 or NaR, or calling this is undefined behaviour.
10+
/// # Safety
11+
///
12+
/// `self` cannot be [0](Self::ZERO) or [NaR](Self::NAR), or calling this function is *undefined
13+
/// behaviour*.
1114
pub(crate) unsafe fn decode_regular(self) -> Decoded<N, ES, Int> {
1215
// This routine is central to nearly every nontrivial algorithm, so it's critical to get right!
1316
// With care, we can make it as small as ~20 instructions and ~7 cycles throughput on a modern

src/posit/encode.rs

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,6 @@ impl<
55
const ES: u32,
66
Int: crate::Int,
77
> Decoded<N, ES, Int> {
8-
const JUNK_BITS: u32 = Posit::<N, ES, Int>::JUNK_BITS;
9-
108
/// Encode a posit, rounding if necessary. The rounding rule is always the same: "round to
119
/// nearest, round ties to even bit pattern, never round to 0 (i.e. never over- or under-flow)".
1210
///
@@ -17,6 +15,11 @@ impl<
1715
/// This function is suitable for encoding a [`Decoded`] that might need rounding to produce a
1816
/// valid Posit (for example, if it was obtained from doing an arithmetic operation). If you
1917
/// don't need to round, see [`Self::encode_regular`].
18+
///
19+
/// # Safety
20+
///
21+
/// [`self.is_normalised()`](Self::is_normalised) has to hold, or calling this function
22+
/// is *undefined behaviour*.
2023
pub(crate) unsafe fn encode_regular_round(self, mut sticky: Int) -> Posit<N, ES, Int> {
2124
debug_assert!(
2225
self.is_normalised(),
@@ -200,6 +203,11 @@ impl<
200203
/// [`Posit::decode_regular`], or that was otherwise crafted as a valid Posit. If if might need
201204
/// rounding (for instance, if you obtained it from doing an arithmetic operation), see
202205
/// [`Self::encode_regular_round`].
206+
///
207+
/// # Safety
208+
///
209+
/// [`self.is_normalised()`](Self::is_normalised) has to hold, or calling this function
210+
/// is *undefined behaviour*.
203211
#[inline]
204212
pub(crate) unsafe fn encode_regular(self) -> Posit<N, ES, Int> {
205213
debug_assert!(

src/posit/ops/add.rs

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,13 @@ impl<
55
const ES: u32,
66
Int: crate::Int,
77
> Posit<N, ES, Int> {
8-
/// `x` and `y` cannot be symmetrical, or calling this function is *undefined behaviour*.
8+
/// Return a [normalised](Decoded::is_normalised) `Decoded` that's the result of adding `x` and
9+
/// `y`, plus the sticky bit.
10+
///
11+
/// # Safety
12+
///
13+
/// `x` and `y` have to be [normalised](Decoded::is_normalised) and cannot be symmetrical, or
14+
/// calling this function is *undefined behaviour*.
915
#[inline]
1016
pub(crate) unsafe fn add_kernel(x: Decoded<N, ES, Int>, y: Decoded<N, ES, Int>) -> (Decoded<N, ES, Int>, Int) {
1117
// Adding two numbers in the form `x.frac × 2^x.exp` and `y.exp × 2^y.exp` is easy, if only
@@ -73,6 +79,7 @@ impl<
7379
// To do this we use our trusty `leading_run_minus_one`, since we want to detect that the
7480
// number starts with n 0s followed by a 1 or n 1s followed by a 0, and shift them so that
7581
// it's just a 01 or a 10.
82+
//
7683
// SAFETY: x and y are not symmetrical (precondition), so `frac` cannot be 0
7784
let underflow = unsafe { frac.leading_run_minus_one() };
7885
let frac = frac << underflow as u32;
@@ -108,7 +115,7 @@ impl<
108115
let b = unsafe { other.decode_regular() };
109116
// SAFETY: `self` and `other` aren't symmetrical
110117
let (result, sticky) = unsafe { Self::add_kernel(a, b) };
111-
// SAFETY: `result` does not have an underflowing `frac`
118+
// SAFETY: `result.is_normalised()` holds
112119
unsafe { result.encode_regular_round(sticky) }
113120
}
114121
}

src/posit/ops/div.rs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,13 @@ impl<
55
const ES: u32,
66
Int: crate::Int,
77
> Posit<N, ES, Int> {
8+
/// Return a [normalised](Decoded::is_normalised) `Decoded` that's the result of dividing `x` by
9+
/// `y`, plus the sticky bit.
10+
///
11+
/// # Safety
12+
///
13+
/// `x` and `y` have to be [normalised](Decoded::is_normalised), or calling this function
14+
/// is *undefined behaviour*.
815
#[inline]
916
pub(crate) unsafe fn div_kernel(x: Decoded<N, ES, Int>, y: Decoded<N, ES, Int>) -> (Decoded<N, ES, Int>, Int) {
1017
// Let's use ÷ to denote true mathematical division, and / denote integer division *that rounds
@@ -58,7 +65,7 @@ impl<
5865
let a = unsafe { self.decode_regular() };
5966
let b = unsafe { other.decode_regular() };
6067
let (result, sticky) = unsafe { Self::div_kernel(a, b) };
61-
// SAFETY: `result` does not have an underflowing `frac`
68+
// SAFETY: `result.is_normalised()` holds
6269
unsafe { result.encode_regular_round(sticky) }
6370
}
6471
}

src/posit/ops/mul.rs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,13 @@ impl<
55
const ES: u32,
66
Int: crate::Int,
77
> Posit<N, ES, Int> {
8+
/// Return a [normalised](Decoded::is_normalised) `Decoded` that's the result of multiplying `x`
9+
/// and `y`, plus the sticky bit.
10+
///
11+
/// # Safety
12+
///
13+
/// `x` and `y` have to be [normalised](Decoded::is_normalised), or calling this function
14+
/// is *undefined behaviour*.
815
#[inline]
916
pub(crate) unsafe fn mul_kernel(x: Decoded<N, ES, Int>, y: Decoded<N, ES, Int>) -> (Decoded<N, ES, Int>, Int) {
1017
// Multiplying two numbers in the form `frac × 2^exp` is much easier than adding them. We have
@@ -63,7 +70,7 @@ impl<
6370
let b = unsafe { other.decode_regular() };
6471
// SAFETY: `self` and `other` aren't symmetrical
6572
let (result, sticky) = unsafe { Self::mul_kernel(a, b) };
66-
// SAFETY: `result` does not have an underflowing `frac`
73+
// SAFETY: `result.is_normalised()` holds
6774
unsafe { result.encode_regular_round(sticky) }
6875
}
6976
}

src/posit/quire/add.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ impl<
2222
///
2323
/// # Safety
2424
///
25-
/// `limbs.len() * size_of::<Int>() + offset < SIZE`, otherwise calling this function
25+
/// `limbs.len() * size_of::<Int>() + offset < SIZE` must hold, or calling this function
2626
/// is *undefined behaviour*.
2727
pub(crate) unsafe fn accumulate<const L: usize, Int: crate::Int>(
2828
&mut self,
@@ -82,7 +82,7 @@ impl<
8282
///
8383
/// # Safety
8484
///
85-
/// `x` must be the result of a [`Posit::decode_regular`] call, otherwise calling this function
85+
/// `x` must be the result of a [`Posit::decode_regular`] call, or calling this function
8686
/// is *undefined behaviour*.
8787
pub(crate) unsafe fn accumulate_decoded<Int: crate::Int>(&mut self, x: Decoded<N, ES, Int>) {
8888
debug_assert!(x.exp <= Posit::<N, ES, Int>::MAX_EXP + Int::ONE);

0 commit comments

Comments
 (0)