Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Sign up
Appearance settings

Commit 398ff24

Browse files
nilehmannranjitjhala
andauthored
Add Flux specifications to path/bstr/hash/time (#438)
This PR adds flux specifications for checking the following modules in core * pat * bstr * hash * time In particular, it verifies that `Nanoseconds` is correctly used with values within the range. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Ranjit Jhala <rjhala@ucsd.edu>
1 parent 88422c8 commit 398ff24

File tree

7 files changed

+121
-4
lines changed

7 files changed

+121
-4
lines changed

‎library/core/Cargo.toml

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,4 +47,11 @@ check-cfg = [
4747

4848
[package.metadata.flux]
4949
enabled = true
50-
include = [ "src/ascii{*.rs,/**/*.rs}" ]
50+
check_overflow = "lazy"
51+
include = [ "src/ascii*.rs",
52+
"src/num/mod.rs",
53+
"src/pat.rs",
54+
"src/bstr/*.rs",
55+
"src/hash/*.rs",
56+
"src/time.rs",
57+
]

‎library/core/src/ascii/ascii_char.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -479,6 +479,7 @@ impl AsciiChar {
479479
/// `b` must be in `0..=127`, or else this is UB.
480480
#[unstable(feature = "ascii_char", issue = "110998")]
481481
#[inline]
482+
#[cfg_attr(flux, flux::spec(fn(b: u8{b <= 127}) -> Self))]
482483
#[requires(b <= 127)]
483484
#[ensures(|result| *result as u8 == b)]
484485
pub const unsafe fn from_u8_unchecked(b: u8) -> Self {
@@ -516,6 +517,10 @@ impl AsciiChar {
516517
/// when writing code using this method, since the implementation doesn't
517518
/// need something really specific, not to make those other arguments do
518519
/// something useful. It might be tightened before stabilization.)
520+
// Only `d < 64` is required for safety as described above, but we use `d < 10` as
521+
// in the `assert_unsafe_precondition` inside. See https://github.com/rust-lang/rust/pull/129374
522+
// for some context about the discrepancy.
523+
#[cfg_attr(flux, flux::spec(fn(d: u8{d < 10}) -> Self))]
519524
#[unstable(feature = "ascii_char", issue = "110998")]
520525
#[inline]
521526
#[track_caller]
@@ -536,8 +541,8 @@ impl AsciiChar {
536541
}
537542

538543
/// Gets this ASCII character as a byte.
544+
#[cfg_attr(flux, flux::spec(fn (Self) -> u8{v: v <= 127}))]
539545
#[unstable(feature = "ascii_char", issue = "110998")]
540-
#[cfg_attr(flux, flux::spec(fn(Self) -> u8{v: v <= 127}))]
541546
#[inline]
542547
pub const fn to_u8(self) -> u8 {
543548
self as u8

‎library/core/src/flux_info.rs

Lines changed: 77 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,87 @@
44
/// See the following link for more information on how extensible properties for primitive operations work:
55
/// <https://flux-rs.github.io/flux/guide/specifications.html#extensible-properties-for-primitive-ops>
66
#[flux::defs {
7+
fn char_to_int(x:char) -> int {
8+
cast(x)
9+
}
10+
711
property ShiftRightByFour[>>](x, y) {
812
16 * [>>](x, 4) == x
913
}
1014
11-
property MaskBy15[&](x, y) {
12-
[&](x, y) <= y
15+
property MaskLess[&](x, y) {
16+
[&](x, y) <= x && [&](x, y) <= y
17+
}
18+
19+
property ShiftLeft[<<](n, k) {
20+
0 < k => n <= [<<](n, k)
21+
}
22+
23+
fn is_ascii_uppercase(n: int) -> bool {
24+
cast('A') <= n && n <= cast('Z')
25+
}
26+
27+
fn is_ascii_lowercase(n: int) -> bool {
28+
cast('a') <= n && n <= cast('z')
29+
}
30+
31+
fn to_ascii_uppercase(n: int) -> int {
32+
n - (cast(is_ascii_lowercase(n)) * 32)
33+
}
34+
35+
fn to_ascii_lowercase(n: int) -> int {
36+
n + (cast(is_ascii_uppercase(n)) * 32)
37+
}
38+
39+
property BitXor0[^](x, y) {
40+
(y == 0) => [^](x, y) == x
41+
}
42+
43+
property BitXor32[^](x, y) {
44+
(is_ascii_lowercase(x) && y == 32) => [^](x, y) == x - 32
45+
}
46+
47+
property BitOr0[|](x, y) {
48+
(y == 0) => [|](x, y) == x
49+
}
50+
51+
property BitOr32[|](x, y) {
52+
(is_ascii_uppercase(x) && y == 32) => [|](x, y) == x + 32
53+
}
54+
55+
}]
56+
#[flux::specs {
57+
mod hash {
58+
mod sip {
59+
struct Hasher {
60+
k0: u64,
61+
k1: u64,
62+
length: usize, // how many bytes we've processed
63+
state: State, // hash State
64+
tail: u64, // unprocessed bytes le
65+
ntail: usize{v: v <= 8}, // how many bytes in tail are valid
66+
_marker: PhantomData<S>,
67+
}
68+
}
69+
70+
impl BuildHasherDefault {
71+
#[trusted(reason="https://github.com/flux-rs/flux/issues/1185")]
72+
fn new() -> Self;
73+
}
74+
}
75+
76+
impl Hasher for hash::sip::Hasher {
77+
fn write(self: &mut Self, msg: &[u8]) ensures self: Self; // mut-ref-unfolding
78+
}
79+
80+
impl Clone for hash::BuildHasherDefault {
81+
#[trusted(reason="https://github.com/flux-rs/flux/issues/1185")]
82+
fn clone(self: &Self) -> Self;
83+
}
84+
85+
impl Debug for time::Duration {
86+
#[trusted(reason="modular arithmetic invariant inside nested fmt_decimal")]
87+
fn fmt(self: &Self, f: &mut fmt::Formatter) -> fmt::Result;
1388
}
1489
}]
1590
const _: () = {};

‎library/core/src/num/mod.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -503,6 +503,7 @@ impl u8 {
503503
/// # Safety
504504
///
505505
/// This byte must be valid ASCII, or else this is UB.
506+
#[cfg_attr(flux, flux::spec(fn({&Self[@n] | n <= 127}) -> _))]
506507
#[must_use]
507508
#[unstable(feature = "ascii_char", issue = "110998")]
508509
#[inline]
@@ -533,6 +534,7 @@ impl u8 {
533534
/// ```
534535
///
535536
/// [`make_ascii_uppercase`]: Self::make_ascii_uppercase
537+
#[cfg_attr(flux, flux::spec(fn(&u8[@n]) -> u8[to_ascii_uppercase(n)]))]
536538
#[must_use = "to uppercase the value in-place, use `make_ascii_uppercase()`"]
537539
#[stable(feature = "ascii_methods_on_intrinsics", since = "1.23.0")]
538540
#[rustc_const_stable(feature = "const_ascii_methods_on_intrinsics", since = "1.52.0")]
@@ -558,6 +560,7 @@ impl u8 {
558560
/// ```
559561
///
560562
/// [`make_ascii_lowercase`]: Self::make_ascii_lowercase
563+
#[cfg_attr(flux, flux::spec(fn(&u8[@n]) -> u8[to_ascii_lowercase(n)]))]
561564
#[must_use = "to lowercase the value in-place, use `make_ascii_lowercase()`"]
562565
#[stable(feature = "ascii_methods_on_intrinsics", since = "1.23.0")]
563566
#[rustc_const_stable(feature = "const_ascii_methods_on_intrinsics", since = "1.52.0")]
@@ -706,6 +709,7 @@ impl u8 {
706709
/// assert!(!lf.is_ascii_uppercase());
707710
/// assert!(!esc.is_ascii_uppercase());
708711
/// ```
712+
#[cfg_attr(flux, flux::spec(fn(&Self[@n]) -> bool[is_ascii_uppercase(n)]))]
709713
#[must_use]
710714
#[stable(feature = "ascii_ctype_on_intrinsics", since = "1.24.0")]
711715
#[rustc_const_stable(feature = "const_ascii_ctype_on_intrinsics", since = "1.47.0")]
@@ -740,6 +744,7 @@ impl u8 {
740744
/// assert!(!lf.is_ascii_lowercase());
741745
/// assert!(!esc.is_ascii_lowercase());
742746
/// ```
747+
#[cfg_attr(flux, flux::spec(fn(&u8[@n]) -> bool[is_ascii_lowercase(n)]))]
743748
#[must_use]
744749
#[stable(feature = "ascii_ctype_on_intrinsics", since = "1.24.0")]
745750
#[rustc_const_stable(feature = "const_ascii_ctype_on_intrinsics", since = "1.47.0")]

‎library/core/src/num/niche_types.rs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,9 @@ macro_rules! define_valid_range_type {
1414
$(#[$m:meta])*
1515
$vis:vis struct $name:ident($int:ident as $uint:ident in $low:literal..=$high:literal);
1616
)+) => {$(
17+
#[cfg_attr(flux, flux::opaque)]
18+
#[cfg_attr(flux, flux::refined_by(val: int))]
19+
#[cfg_attr(flux, flux::invariant($low <= cast(val) && cast(val) <= $high))]
1720
#[derive(Clone, Copy, Eq)]
1821
#[repr(transparent)]
1922
#[rustc_layout_scalar_valid_range_start($low)]
@@ -33,6 +36,7 @@ macro_rules! define_valid_range_type {
3336

3437
impl $name {
3538
#[inline]
39+
#[cfg_attr(flux, flux::spec(fn (val: $int) -> Option<Self[{val: cast(val)}]>))]
3640
pub const fn new(val: $int) -> Option<Self> {
3741
if (val as $uint) >= ($low as $uint) && (val as $uint) <= ($high as $uint) {
3842
// SAFETY: just checked the inclusive range
@@ -49,12 +53,14 @@ macro_rules! define_valid_range_type {
4953
/// Immediate language UB if `val` is not within the valid range for this
5054
/// type, as it violates the validity invariant.
5155
#[inline]
56+
#[cfg_attr(flux, flux::spec(fn (val: $int{ $low <= cast(val) && cast(val) <= $high }) -> Self[{val:cast(val)}]))]
5257
pub const unsafe fn new_unchecked(val: $int) -> Self {
5358
// SAFETY: Caller promised that `val` is within the valid range.
5459
unsafe { $name(val) }
5560
}
5661

5762
#[inline]
63+
#[cfg_attr(flux, flux::spec(fn (self: Self) -> $int[cast(self.val)] ensures $low <= cast(self.val) && cast(self.val) <= $high))]
5864
pub const fn as_inner(self) -> $int {
5965
// SAFETY: This is a transparent wrapper, so unwrapping it is sound
6066
// (Not using `.0` due to MCP#807.)

‎library/core/src/num/uint_macros.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -629,6 +629,7 @@ macro_rules! uint_impl {
629629
without modifying the original"]
630630
#[inline(always)]
631631
#[track_caller]
632+
#[cfg_attr(flux, flux::spec(fn(self: Self, rhs: Self{self + rhs <= $MaxV}) -> Self[self + rhs]))]
632633
#[requires(!self.overflowing_add(rhs).1)]
633634
pub const unsafe fn unchecked_add(self, rhs: Self) -> Self {
634635
assert_unsafe_precondition!(

‎library/core/src/pat.rs

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,22 @@ macro_rules! pattern_type {
1313
};
1414
}
1515

16+
// The Flux spec for the `trait RangePattern` below uses
17+
// [associated refinements](https://flux-rs.github.io/flux/tutorial/08-traits.html)
18+
// The `sub_one` method may only be safe for certain values,
19+
// e.g. when the value is not the "minimum of the type" as in the
20+
// case of the `char` implementation below. To specify this precondition generically
21+
// 1. at the trait level, we introduce the predicate `sub_ok`
22+
// which characterizes the "valid" values at which `sub_one`
23+
// can be safely called, and by default, specify this predicate
24+
// is "true";
25+
// 2. at the impl level, we can provide a type-specific implementation
26+
// of `sub_ok` that permits the verification of the impl for that type.
27+
1628
/// A trait implemented for integer types and `char`.
1729
/// Useful in the future for generic pattern types, but
1830
/// used right now to simplify ast lowering of pattern type ranges.
31+
#[cfg_attr(flux, flux::assoc(fn sub_ok(self: Self) -> bool { true }))]
1932
#[unstable(feature = "pattern_type_range_trait", issue = "123646")]
2033
#[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")]
2134
#[const_trait]
@@ -33,6 +46,7 @@ pub trait RangePattern {
3346
const MAX: Self;
3447

3548
/// A compile-time helper to subtract 1 for exclusive ranges.
49+
#[cfg_attr(flux, flux::spec(fn (self: Self{<Self as RangePattern>::sub_ok(self)}) -> Self))]
3650
#[lang = "RangeSub"]
3751
#[track_caller]
3852
fn sub_one(self) -> Self;
@@ -61,12 +75,16 @@ impl_range_pat! {
6175
u8, u16, u32, u64, u128, usize,
6276
}
6377

78+
// The "associated refinement" `sub_ok` is defined as `non-zero` for `char`, to let Flux
79+
// verify that the `self as u32 -1` in the impl does not underflow.
80+
#[cfg_attr(flux, flux::assoc(fn sub_ok(self: char) -> bool { 0 < char_to_int(self)}))]
6481
#[rustc_const_unstable(feature = "pattern_type_range_trait", issue = "123646")]
6582
impl const RangePattern for char {
6683
const MIN: Self = char::MIN;
6784

6885
const MAX: Self = char::MAX;
6986

87+
#[cfg_attr(flux, flux::spec(fn (self: char{<char as RangePattern>::sub_ok(self)}) -> char))]
7088
fn sub_one(self) -> Self {
7189
match char::from_u32(self as u32 - 1) {
7290
None => panic!("exclusive range to start of valid chars"),

0 commit comments

Comments
(0)

AltStyle によって変換されたページ (->オリジナル) /