ostd/mm/frame/
segment.rs

1// SPDX-License-Identifier: MPL-2.0
2//! A contiguous range of frames.
3use vstd::{
4    prelude::*,
5    simple_pptr::{PPtr, PointsTo},
6    std_specs::{convert::FromSpecImpl, iter::IteratorSpecImpl},
7};
8use vstd_extra::{assert, cast_ptr::*, ownership::*, panic::may_panic, prelude::*};
9
10use crate::specs::{
11    arch::*,
12    mm::frame::{
13        frame_specs::FrameRawPerms,
14        mapping::{frame_to_index, group_page_meta, index_to_meta},
15        meta_owners::*,
16        meta_region_owners::MetaRegionOwners,
17        segment::*,
18    },
19};
20
21use super::{
22    Frame, Paddr,
23    meta::mapping::frame_to_meta,
24    meta::{AnyFrameMeta, GetFrameError},
25};
26use crate::mm::frame::{meta::REF_COUNT_MAX, untyped::AnyUFrameMeta};
27use crate::mm::page_table::RCClone;
28use crate::mm::{PagingLevel, Vaddr, frame::MetaSlot, paddr_to_vaddr};
29use core::{fmt::Debug, mem::ManuallyDrop, ops::Range};
30
31verus! {
32
33/// A contiguous range of homogeneous physical memory frames.
34///
35/// This is a handle to multiple contiguous frames. It will be more lightweight
36/// than owning an array of frame handles.
37///
38/// The ownership is achieved by the reference counting mechanism of frames.
39/// When constructing a [`Segment`], the frame handles are created then
40/// forgotten, leaving the reference count. When dropping a it, the frame
41/// handles are restored and dropped, decrementing the reference count.
42///
43/// All the metadata of the frames are homogeneous, i.e., they are of the same
44/// type.
45// #[repr(transparent)]
46pub struct Segment<M: AnyFrameMeta + ?Sized> {
47    range: Range<Paddr>,
48    _marker: core::marker::PhantomData<M>,
49    /// One raw permission bundle for each frame in `range`, in address order.
50    #[cfg(verus_keep_ghost_body)]
51    tracked_perms: Tracked<Option<Seq<FrameRawPerms>>>,
52}
53
54/*
55impl<M: AnyFrameMeta + ?Sized> Debug for Segment<M> {
56    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
57        write!(f, "Segment({:#x}..{:#x})", self.range.start, self.range.end)
58    }
59}
60*/
61
62/*impl<M: AnyFrameMeta + ?Sized> Drop for Segment<M> {
63    fn drop(&mut self) {
64        for paddr in self.range.clone().step_by(PAGE_SIZE) {
65            // SAFETY: for each frame there would be a forgotten handle
66            // when creating the `Segment` object.
67            drop(unsafe { Frame::<M>::from_raw(paddr) });
68        }
69    }
70}*/
71
72/// A contiguous range of homogeneous untyped physical memory frames that have any metadata.
73///
74/// In other words, the metadata of the frames are of the same type, and they
75/// are untyped, but the type of metadata is not known at compile time. An
76/// [`USegment`] as a parameter accepts any untyped segments.
77///
78/// The usage of this frame will not be changed while this object is alive.
79pub type USegment = Segment<dyn AnyUFrameMeta>;
80
81/* impl<M: AnyFrameMeta + ?Sized> Clone for Segment<M> {
82    fn clone(&self) -> Self {
83        for paddr in self.range.clone().step_by(PAGE_SIZE) {
84            // SAFETY: for each frame there would be a forgotten handle
85            // when creating the `Segment` object, so we already have
86            // reference counts for the frames.
87            unsafe { inc_frame_ref_count(paddr) };
88        }
89        Self {
90            range: self.range.clone(),
91            _marker: core::marker::PhantomData,
92        }
93    }
94} */
95
96impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> RCClone for Segment<M> {
97    open spec fn clone_requires(self, perm: MetaRegionOwners) -> bool {
98        &&& self.inv()
99        &&& perm.inv()
100        &&& self.relate_regions(perm)
101        &&& forall|pa: Paddr|
102            #![trigger frame_to_index(pa)]
103            (self.start_paddr() <= pa < self.end_paddr() && pa % PAGE_SIZE == 0) ==> {
104                let idx = frame_to_index(pa);
105                &&& perm.contains(idx)
106                &&& valid_frame_paddr(pa)
107                &&& perm.ref_count(idx) > 0
108                &&& perm.ref_count(idx) + 1 < REF_COUNT_MAX
109                &&& !MetaSlot::inc_ref_count_panic_cond(perm.slot_owners[idx].ref_count_perm)
110            }
111    }
112
113    open spec fn clone_ensures(
114        self,
115        old_perm: MetaRegionOwners,
116        new_perm: MetaRegionOwners,
117        res: Self,
118    ) -> bool {
119        &&& res.range() == self.range()
120        &&& res.inv()
121        &&& new_perm.inv()
122        &&& res.relate_regions(new_perm)
123    }
124
125    #[verifier::loop_isolation(false)]
126    #[verifier::rlimit(200)]
127    fn clone(&self, Tracked(perm): Tracked<&mut MetaRegionOwners>) -> (res: Self) {
128        let mut paddr = self.range.start;
129        proof_decl! {
130            let tracked mut raw_perms = Seq::<FrameRawPerms>::tracked_empty();
131        }
132
133        loop
134            invariant
135                perm.inv(),
136                self.inv(),
137                perm.slots == old(perm).slots,
138                perm.slot_owners.dom() == old(perm).slot_owners.dom(),
139                raw_perms.len() == (paddr - self.range.start) / (PAGE_SIZE as int),
140                forall|i: int|
141                    #![trigger raw_perms[i]]
142                    0 <= i < raw_perms.len() ==> {
143                        let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
144                        &&& raw_perms[i].slot_perm == perm.slots[idx]
145                        &&& raw_perms[i].inv()
146                        &&& raw_perms[i].metadata_perm.id()
147                            == perm.slot_owners[idx].metadata_perm.id()
148                    },
149                forall|i: int|
150                    #![trigger frame_to_index((self.range.start + i * PAGE_SIZE) as usize)]
151                    0 <= i < raw_perms.len() ==> ({
152                        let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
153                        &&& perm.contains(idx)
154                        &&& perm.slot_owners[idx].slot_vaddr == index_to_meta(idx)
155                        &&& perm.ref_count(idx) > 0
156                        &&& perm.ref_count(idx) <= REF_COUNT_MAX
157                        &&& perm.slot_owners[idx].paths_in_pt.is_empty()
158                        &&& perm.slot_owners[idx].usage is Frame
159                    }),
160                self.range.start <= paddr <= self.range.end,
161                paddr % PAGE_SIZE == 0,
162                paddr <= MAX_PADDR,
163                forall|pa: Paddr|
164                    #![trigger frame_to_index(pa)]
165                    (paddr <= pa < self.range.end && pa % PAGE_SIZE == 0) ==> {
166                        let idx = frame_to_index(pa);
167                        &&& perm.contains(idx)
168                        &&& valid_frame_paddr(pa)
169                        &&& perm.ref_count(idx) > 0
170                        &&& perm.ref_count(idx) + 1 < REF_COUNT_MAX
171                        &&& !MetaSlot::inc_ref_count_panic_cond(
172                            perm.slot_owners[idx].ref_count_perm,
173                        )
174                    },
175                forall|i: int|
176                    #![trigger frame_to_index((self.range.start + i * PAGE_SIZE) as usize)]
177                    raw_perms.len() <= i < self.len() ==> perm.slot_owner(
178                        (self.range.start + i * PAGE_SIZE) as usize,
179                    ) == old(perm).slot_owner((self.range.start + i * PAGE_SIZE) as usize),
180            decreases self.range.end - paddr,
181        {
182            if paddr >= self.range.end {
183                break;
184            }
185            let tracked_permission = unsafe {
186                #[verus_spec(with Tracked(perm))]
187                crate::mm::frame::inc_frame_ref_count(paddr)
188            };
189            let tracked frame_permission = tracked_permission.get();
190            proof {
191                let tracked slot_perm = perm.tracked_borrow_slot(paddr);
192                raw_perms.tracked_push(
193                    FrameRawPerms { slot_perm, metadata_perm: frame_permission },
194                );
195            }
196
197            paddr += PAGE_SIZE;
198        }
199
200        Self {
201            range: self.range.start..self.range.end,
202            _marker: core::marker::PhantomData,
203            #[cfg(verus_keep_ghost_body)]
204            tracked_perms: Tracked(Some(raw_perms)),
205        }
206    }
207}
208
209#[verus_verify]
210impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Segment<M> {
211    /// Creates a new [`Segment`] from unused frames.
212    ///
213    /// The caller must provide a closure to initialize metadata for all the frames.
214    /// The closure receives the physical address of the frame and returns the
215    /// metadata, which is similar to [`core::array::from_fn`].
216    ///
217    /// It returns an error if:
218    ///  - the physical address is invalid or not aligned;
219    ///  - any of the frames cannot be created with a specific reason.
220    ///
221    /// # Panics
222    ///
223    /// It panics if the range is empty.
224    ///
225    /// # Verified Properties
226    /// ## Preconditions
227    /// - the metadata function must be well-formed and valid for all frames in the range;
228    /// - the metadata function must ensure that the frames can be created and owned by the segment;
229    /// - for any frame created via the closure `metadata_fn`, the corresponding slot in `regions`
230    ///   must be unused and not dropped in the owner ([`MetaRegionOwners`]).
231    ///
232    /// Range constraints (alignment, `range.end <= MAX_PADDR`, non-emptiness) are runtime-checked
233    /// in the body — see the postconditions below for the corresponding error variants.
234    /// ## Postconditions
235    /// - if the result is `Ok`, the returned segment satisfies its invariant,
236    ///   relates to the updated metadata region, and has the same physical
237    ///   address range as the input;
238    /// - if the input range is misaligned, the result is `Err(NotAligned)`;
239    /// - if the input range exceeds `MAX_PADDR`, the result is `Err(OutOfBound)`;
240    /// - if the input is aligned and within `MAX_PADDR` and the function terminated,
241    ///   then `range.start < range.end` (the runtime `assert!` would otherwise diverge).
242    /// FIXME: this implementation does not match source code.
243    #[verifier::spinoff_prover]
244    #[verifier::loop_isolation(false)]
245    #[verifier::allow_complex_invariants]
246    #[verus_spec(r =>
247        with
248            Tracked(regions): Tracked<&mut MetaRegionOwners>,
249            Tracked(repr_perm): Tracked<&mut M::ReprPerm>,
250        requires
251            old(regions).inv(),
252            forall|paddr_in: Paddr|
253                (range.start <= paddr_in < range.end && paddr_in % PAGE_SIZE == 0) ==> {
254                    &&& metadata_fn.requires((paddr_in,))
255                },
256            forall|paddr_in: Paddr, paddr_out: Paddr, m: M|
257                metadata_fn.ensures((paddr_in,), (paddr_out, m)) ==> paddr_in == paddr_out,
258            !(range.end <= MAX_PADDR ==> range.start < range.end) ==> may_panic(),
259        ensures
260            final(regions).inv(),
261            (range.start % PAGE_SIZE != 0 || range.end % PAGE_SIZE != 0)
262                ==> r == Err::<Self, _>(GetFrameError::NotAligned),
263            (range.start % PAGE_SIZE == 0 && range.end % PAGE_SIZE == 0 && range.end > MAX_PADDR)
264                ==> r == Err::<Self, _>(GetFrameError::OutOfBound),
265            r matches Ok(seg) ==> {
266                &&& seg.inv()
267                &&& seg.start_paddr() == range.start
268                &&& seg.end_paddr() == range.end
269                &&& seg.start_paddr() < seg.end_paddr()
270                &&& seg.relate_regions(*final(regions))
271                &&& forall|paddr: Paddr|
272                    #![trigger frame_to_index(paddr)]
273                    (range.start <= paddr < range.end && paddr % PAGE_SIZE == 0)
274                        ==> final(regions).contains(frame_to_index(paddr))
275                &&& range.start < range.end <= MAX_PADDR
276            },
277    )]
278    pub fn from_unused(range: Range<Paddr>, metadata_fn: impl Fn(Paddr) -> (Paddr, M)) -> (res:
279        Result<Self, GetFrameError>) {
280        proof_decl! {
281            let tracked mut addrs = Seq::<usize>::tracked_empty();
282            let tracked raw_perms = Seq::<FrameRawPerms>::tracked_empty();
283        }
284
285        if range.start % PAGE_SIZE != 0 || range.end % PAGE_SIZE != 0 {
286            return Err(GetFrameError::NotAligned);
287        }
288        if range.end > MAX_PADDR {
289            return Err(GetFrameError::OutOfBound);
290        }
291        assert!(range.start < range.end);
292
293        // Construct a segment early to recycle previously forgotten frames if
294        // the subsequent operations fails in the middle.
295
296        proof_with!{ tracked_perms: Tracked(Some(raw_perms)) }
297        let mut segment = Self {
298            range: range.start..range.start,
299            _marker: core::marker::PhantomData,
300        };
301
302        let mut i = 0;
303        let addr_len = (range.end - range.start) / PAGE_SIZE;
304
305        while i < addr_len
306            invariant
307                segment.tracked_perms@ is Some,
308                i <= addr_len,
309                i == addrs.len(),
310                i == segment.tracked_perms@->0.len(),
311                range.start <= range.start + i * PAGE_SIZE <= range.end,
312                range.end == range.start + addr_len * PAGE_SIZE,
313                addr_len == (range.end - range.start) / PAGE_SIZE as int,
314                i <= addr_len,
315                forall|paddr_in: Paddr|
316                    (range.start + i * PAGE_SIZE <= paddr_in < range.end && paddr_in % PAGE_SIZE
317                        == 0) ==> {
318                        &&& metadata_fn.requires((paddr_in,))
319                    },
320                forall|paddr_in: Paddr, paddr_out: Paddr, m: M|
321                    range.start + i * PAGE_SIZE <= paddr_in < range.end && paddr_in % PAGE_SIZE == 0
322                        && metadata_fn.ensures((paddr_in,), (paddr_out, m)) ==> paddr_in
323                        == paddr_out,
324                forall|j: int|
325                    #![trigger addrs[j]]
326                    0 <= j < addrs.len() ==> {
327                        let idx = frame_to_index(addrs[j]);
328                        &&& regions.contains(idx)
329                        &&& regions.slot_owners[idx].slot_vaddr == index_to_meta(idx)
330                        &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX
331                        &&& segment.tracked_perms@->0[j].inv()
332                        &&& segment.tracked_perms@->0[j].slot_perm == regions.slots[idx]
333                        &&& segment.tracked_perms@->0[j].metadata_perm.id()
334                            == regions.slot_owners[idx].metadata_perm.id()
335                        &&& regions.slot_owners[idx].paths_in_pt.is_empty()
336                        &&& regions.slot_owners[idx].usage is Frame
337                        &&& addrs[j] % PAGE_SIZE == 0
338                        &&& addrs[j] < MAX_PADDR
339                        &&& addrs[j] == range.start + (j as u64) * PAGE_SIZE
340                    },
341                regions.inv(),
342                regions.slot_owners.dom() == old(regions).slot_owners.dom(),
343                segment.range.end == range.start + i * PAGE_SIZE,
344            ensures
345                i == addr_len,
346            decreases addr_len - i,
347        {
348            let paddr_in = range.start + i * PAGE_SIZE;
349            let (paddr, meta) = metadata_fn(paddr_in);
350
351            let ghost regions_pre = *regions;
352            let res = #[verus_spec(with Tracked(regions), Tracked(repr_perm))]
353            Frame::<M>::from_unused(paddr, meta);
354            let mut frame = match res {
355                Ok(f) => f,
356                Err(e) => {
357                    let mut p = range.start;
358                    let ghost mut k: int = 0;
359                    while p < segment.range.end
360                        invariant
361                            regions.inv(),
362                            segment.tracked_perms@->0.len() == i - k,
363                            regions.slot_owners.dom() == old(regions).slot_owners.dom(),
364                            range.start % PAGE_SIZE == 0,
365                            i == addrs.len(),
366                            segment.range.end == range.start + i * PAGE_SIZE,
367                            range.start <= p <= segment.range.end,
368                            p == range.start + k * PAGE_SIZE,
369                            p % PAGE_SIZE == 0,
370                            0 <= k <= i,
371                            forall|j: int|
372                                #![trigger addrs[j]]
373                                k <= j < addrs.len() ==> {
374                                    let idx = frame_to_index(addrs[j]);
375                                    &&& regions.contains(idx)
376                                    &&& regions.slot_owners[idx].slot_vaddr == index_to_meta(idx)
377                                    &&& 0 < regions.ref_count(idx) <= REF_COUNT_MAX
378                                    &&& segment.tracked_perms@ is Some
379                                    &&& segment.tracked_perms@->0[j - k].inv()
380                                    &&& segment.tracked_perms@->0[j - k].slot_perm
381                                        == regions.slots[idx]
382                                    &&& segment.tracked_perms@->0[j - k].metadata_perm.id()
383                                        == regions.slot_owners[idx].metadata_perm.id()
384                                    &&& regions.slot_owners[idx].paths_in_pt.is_empty()
385                                    &&& regions.slot_owners[idx].usage is Frame
386                                    &&& addrs[j] % PAGE_SIZE == 0
387                                    &&& addrs[j] < MAX_PADDR
388                                    &&& addrs[j] == range.start + (j as u64) * PAGE_SIZE
389                                },
390                        decreases segment.range.end - p,
391                    {
392                        proof {
393                            broadcast use group_page_meta;
394
395                            assert(addrs[k] == p);
396
397                        }
398                        let tracked perm =
399                            segment.tracked_perms.tracked_borrow_mut().tracked_pop_front();
400                        let frame = unsafe {
401                            #[verus_spec(with Tracked(perm))]
402                            Frame::<M>::from_raw(p)
403                        };
404                        frame.drop(Tracked(regions));
405                        p += PAGE_SIZE;
406                        proof {
407                            k = k + 1;
408                        }
409                    }
410                    return Err(e);
411                },
412            };
413
414            proof_decl! {
415                let tracked frame_permission: FracMetadataPerm = frame.tracked_metadata_perm.tracked_take();
416                let tracked slot_perm = *frame.tracked_slot_perm;
417            }
418            let _ = ManuallyDrop::new(frame);
419            segment.range.end = paddr + PAGE_SIZE;
420            proof {
421                broadcast use group_page_meta;
422
423                let idx = frame_to_index(paddr);
424                axiom_mmio_usage_iff_mmio_paddr(regions.slot_owners[idx]);
425                axiom_mmio_usage_iff_mmio_paddr(regions_pre.slot_owners[idx]);
426                addrs.tracked_push(paddr);
427                segment.tracked_perms.tracked_borrow_mut().tracked_push(
428                    FrameRawPerms { slot_perm, metadata_perm: frame_permission },
429                );
430            }
431
432            i += 1;
433        }
434
435        proof {
436            assert forall|addr: usize|
437                #![trigger frame_to_index(addr)]
438                range.start <= addr < range.end && addr % PAGE_SIZE == 0 implies {
439                regions.contains(frame_to_index(addr))
440            } by {
441                let j = (addr - range.start) / PAGE_SIZE as int;
442                assert(addrs[j as int] == addr);
443            }
444            assert forall|i: int|
445                #![trigger frame_to_index((segment.range.start + i * PAGE_SIZE) as usize)]
446                0 <= i < segment.len() implies {
447                let idx = frame_to_index((segment.range.start + i * PAGE_SIZE) as usize);
448                &&& segment.tracked_perms@->0[i].inv()
449                &&& segment.tracked_perms@->0[i].slot_perm == regions.slots[idx]
450                &&& segment.tracked_perms@->0[i].metadata_perm.id()
451                    == regions.slot_owners[idx].metadata_perm.id()
452                &&& regions.contains(idx)
453                &&& regions.slot_owners[idx].slot_vaddr == index_to_meta(idx)
454                &&& regions.ref_count(idx) > 0
455                &&& regions.ref_count(idx) <= REF_COUNT_MAX
456                &&& regions.slot_owners[idx].paths_in_pt.is_empty()
457                &&& regions.slot_owners[idx].usage is Frame
458            } by {
459                assert(addrs[i] == segment.range.start + i * PAGE_SIZE);
460            }
461
462        }
463
464        Ok(segment)
465    }
466
467    /// Restores the [`Segment`] from the raw physical address range.
468    ///
469    /// # Verified Properties
470    /// ## Preconditions
471    ///
472    /// ## Postconditions
473    /// - the returned segment satisfies its invariant;
474    /// - the returned segment has the same physical address range as the input;
475    ///
476    /// # Safety
477    ///
478    /// The range must be a forgotten [`Segment`] that matches the type `M`.
479    /// The caller must ensure the range was previously produced by [`Self::into_raw`]
480    /// and that the metadata region still records the segment obligations.
481    #[verus_spec(r =>
482        with
483            Tracked(raw_perms): Tracked<Seq<FrameRawPerms>>,
484        requires
485            range.start % PAGE_SIZE == 0,
486            range.end % PAGE_SIZE == 0,
487            range.start <= range.end <= MAX_PADDR,
488            raw_perms.len() == (range.end - range.start) / PAGE_SIZE as int,
489            forall |i: int| #![trigger raw_perms[i]]
490                0 <= i < raw_perms.len() ==> {
491                    let paddr = (range.start + i * PAGE_SIZE) as usize;
492                    &&& raw_perms[i].slot_vaddr() == frame_to_meta(paddr)
493                    &&& raw_perms[i].inv()
494                },
495        ensures
496            r.inv(),
497            r.range() == range,
498    )]
499    pub(crate) unsafe fn from_raw(range: Range<Paddr>) -> Self {
500        proof_with!{ tracked_perms: Tracked(Some(raw_perms)) }
501        Self { range, _marker: core::marker::PhantomData }
502    }
503}
504
505#[verus_verify]
506impl<M: AnyFrameMeta + ?Sized> Segment<M> {
507    /// Gets the start physical address of the contiguous frames.
508    #[verus_verify(dual_spec)]
509    #[verus_spec(
510        returns
511            self.start_paddr(),
512    )]
513    pub fn start_paddr(&self) -> Paddr {
514        self.range.start
515    }
516
517    /// Gets the end physical address of the contiguous frames.
518    #[verus_verify(dual_spec)]
519    #[verus_spec(
520        returns
521            self.end_paddr(),
522    )]
523    pub fn end_paddr(&self) -> Paddr {
524        self.range.end
525    }
526
527    /// Gets the length in bytes of the contiguous frames.
528    #[verus_verify(dual_spec)]
529    #[verus_spec(r =>
530        requires
531            self.inv(),
532        ensures
533            r == self.end_paddr() - self.start_paddr(),
534        returns
535            self.size()
536    )]
537    pub fn size(&self) -> usize {
538        self.range.end - self.range.start
539    }
540
541    pub open spec fn range(&self) -> Range<Paddr> {
542        self.start_paddr()..self.end_paddr()
543    }
544
545    /// Returns the number of pages of the contiguous frames.
546    pub open spec fn len(&self) -> int {
547        (self.size() / PAGE_SIZE) as int
548    }
549
550    pub closed spec fn raw_perms(&self) -> Seq<FrameRawPerms> {
551        self.tracked_perms@->0
552    }
553
554    pub open spec fn metadata_perms(&self) -> Seq<FracMetadataPerm> {
555        self.raw_perms().map_values(|perm: FrameRawPerms| perm.metadata_perm)
556    }
557
558    pub closed spec fn inner_perm_inv(&self) -> bool {
559        self.tracked_perms@ is Some
560    }
561
562    pub open spec fn slot_perms(&self) -> Seq<&'static PointsTo<MetaSlot>> {
563        self.raw_perms().map_values(|perm: FrameRawPerms| perm.slot_perm)
564    }
565}
566
567#[verus_verify]
568impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Segment<M> {
569    /// Splits the frames into two at the given byte offset from the start.
570    ///
571    /// The resulting frames cannot be empty. So the offset cannot be neither
572    /// zero nor the length of the frames.
573    ///
574    /// # Verified Properties
575    /// ## Preconditions
576    /// - the segment must satisfy its invariant;
577    /// - the offset must be aligned and within bounds;
578    ///
579    /// ## Postconditions
580    /// - the resulting segments satisfy their invariants;
581    /// - they match [`Self::split_spec`].
582    #[verus_spec(r =>
583        requires
584            self.inv(),
585            offset % PAGE_SIZE != 0 ==> may_panic(),
586            !(0 < offset && offset < self.size()) ==> may_panic(),
587        ensures
588            (r.0, r.1) == self.split_spec(offset),
589    )]
590    #[verifier::spinoff_prover]
591    pub fn split(mut self, offset: usize) -> (Self, Self) {
592        assert!(offset % PAGE_SIZE == 0);
593        assert!(0 < offset && offset < self.size());
594
595        let tracked mut left_perms = self.tracked_perms.tracked_take();
596        let tracked right_perms = seq_tracked_split_at(
597            &mut left_perms,
598            (offset / PAGE_SIZE) as int,
599        );
600        let old = ManuallyDrop::new(self);
601        let at = old.range.start + offset;
602
603        (
604            Self {
605                range: old.range.start..at,
606                _marker: core::marker::PhantomData,
607                #[cfg(verus_keep_ghost_body)]
608                tracked_perms: Tracked(Some(left_perms)),
609            },
610            Self {
611                range: at..old.range.end,
612                _marker: core::marker::PhantomData,
613                #[cfg(verus_keep_ghost_body)]
614                tracked_perms: Tracked(Some(right_perms)),
615            },
616        )
617    }
618
619    /// Precise panic condition for [`Self::slice`]. `slice` diverges iff:
620    ///  - the slice range is misaligned, reversed, or out of the segment's
621    ///    bounds (the diverging `assert!`s at the top of `slice`), or
622    ///  - **the specific per-frame slot that `slice` bumps** is already
623    ///    saturated (`inc_ref_count` would overflow). Unlike `query` which
624    ///    clones one item, `slice` bumps one refcount per page in the
625    ///    slice range, so the saturation disjunct is an *exists* over those
626    ///    specific paddrs `self.range.start + j * PAGE_SIZE` for
627    ///    `j ∈ [range.start/PAGE_SIZE, range.end/PAGE_SIZE)`.
628    pub open spec fn page_in_range_saturated(
629        self,
630        range: &Range<usize>,
631        regions: MetaRegionOwners,
632    ) -> bool {
633        exists|j: int|
634            #![trigger frame_to_index((self.start_paddr() + j * PAGE_SIZE) as usize)]
635            (range.start as int) / (PAGE_SIZE as int) <= j < (range.end as int) / (PAGE_SIZE as int)
636                && regions.slot_owner((self.start_paddr() + j * PAGE_SIZE) as usize).ref_count()
637                >= REF_COUNT_MAX
638    }
639
640    // [FIXED] BUG FOUND BY FV: potential overflow. https://github.com/asterinas/asterinas/pull/3587
641    /// Gets an extra handle to the frames in the byte offset range.
642    ///
643    /// The sliced byte offset range in indexed by the offset from the start of
644    /// the contiguous frames. The resulting frames holds extra reference counts.
645    ///
646    /// # Verified Properties
647    /// ## Postconditions
648    /// - the resulting slice's range matches the slicing range and is in-bounds
649    ///   (the in-bounds check follows from the diverging `assert!` in the body);
650    /// - `regions` preserves invariants and key domains. Per-frame state for a
651    ///   hypothetical sub-segment relation is not exposed; threading that through
652    ///   the per-frame ref-count bump loop would require a much heavier proof.
653    ///   Mirrors [`Segment::clone`].
654    ///
655    /// See also [`vstd::seq::Seq::subrange`].
656    #[verus_spec(r =>
657        with
658            Tracked(regions): Tracked<&mut MetaRegionOwners>,
659        requires
660            self.inv(),
661            old(regions).inv(),
662            self.relate_regions(*old(regions)),
663            range.start % PAGE_SIZE != 0 ==> may_panic(),
664            range.end % PAGE_SIZE != 0 ==> may_panic(),
665            range.start > range.end ==> may_panic(),
666            range.end > self.size() ==> may_panic(),
667            self.page_in_range_saturated(range, *old(regions)) ==> may_panic(),
668        ensures
669            range.start % PAGE_SIZE == 0,
670            range.end % PAGE_SIZE == 0,
671            range.start <= range.end,
672            self.start_paddr() + range.end <= self.end_paddr(),
673            !self.page_in_range_saturated(range, *old(regions)),
674            r.inv(),
675            r.start_paddr() == self.start_paddr() + range.start,
676            r.end_paddr() == self.start_paddr() + range.end,
677            r.end_paddr() <= self.end_paddr(),
678            final(regions).inv(),
679            final(regions).slots == old(regions).slots,
680            final(regions).slot_owners.dom() == old(regions).slot_owners.dom(),
681            r.relate_regions(*final(regions)),
682    )]
683    #[verifier::spinoff_prover]
684    #[verifier::loop_isolation(false)]
685    #[verifier::rlimit(200)]
686    pub fn slice(&self, range: &Range<usize>) -> Self {
687        assert!(range.start % PAGE_SIZE == 0 && range.end % PAGE_SIZE == 0);
688        assert!(range.start <= range.end && range.end <= self.size());
689        let start = self.range.start + range.start;
690        let end = self.range.start + range.end;
691
692        let mut paddr = start;
693        let ghost addr_len = (end - start) / PAGE_SIZE as int;
694        let ghost first_perm_idx: int = (range.start / PAGE_SIZE) as int;
695        let ghost last_perm_idx: int = (range.end / PAGE_SIZE) as int;
696        let ghost mut i: int = 0;
697        proof_decl! {
698            let tracked mut raw_perms = Seq::<FrameRawPerms>::tracked_empty();
699        }
700        loop
701            invariant
702                self.page_in_range_saturated(range, *old(regions)) ==> may_panic(),
703                regions.inv(),
704                regions.slots == old(regions).slots,
705                regions.slot_owners.dom() == old(regions).slot_owners.dom(),
706                raw_perms.len() == i,
707                forall|j: int|
708                    #![trigger raw_perms[j]]
709                    0 <= j < raw_perms.len() ==> {
710                        let idx = frame_to_index((start + j * PAGE_SIZE) as usize);
711                        &&& raw_perms[j].slot_perm == regions.slots[idx]
712                        &&& raw_perms[j].inv()
713                        &&& raw_perms[j].metadata_perm.id()
714                            == regions.slot_owners[idx].metadata_perm.id()
715                    },
716                forall|j: int|
717                    #![trigger frame_to_index((start + j * PAGE_SIZE) as usize)]
718                    0 <= j < raw_perms.len() ==> {
719                        let idx = frame_to_index((start + j * PAGE_SIZE) as usize);
720                        &&& regions.contains(idx)
721                        &&& regions.slot_owners[idx].slot_vaddr == index_to_meta(idx)
722                        &&& regions.ref_count(idx) > 0
723                        &&& regions.ref_count(idx) <= REF_COUNT_MAX
724                        &&& regions.slot_owners[idx].paths_in_pt.is_empty()
725                        &&& regions.slot_owners[idx].usage is Frame
726                    },
727                paddr == (start + i * PAGE_SIZE) as usize,
728                paddr <= end,
729                0 <= i <= addr_len,
730                paddr < end <==> i < addr_len,
731                forall|j: int|
732                    #![trigger frame_to_index((self.range.start + j * PAGE_SIZE) as usize)]
733                    first_perm_idx + i <= j < last_perm_idx ==> (*regions).slot_owner(
734                        (self.range.start + j * PAGE_SIZE) as usize,
735                    ) == old(regions).slot_owner((self.range.start + j * PAGE_SIZE) as usize),
736                forall|j: int|
737                    #![trigger frame_to_index((self.range.start + j * PAGE_SIZE) as usize)]
738                    first_perm_idx <= j < first_perm_idx + i ==> old(regions).slot_owner(
739                        (self.range.start + j * PAGE_SIZE) as usize,
740                    ).ref_count() < REF_COUNT_MAX,
741            decreases addr_len - i,
742        {
743            if paddr >= end {
744                break;
745            }
746            let ghost perm_idx: int = first_perm_idx + i;
747
748            proof {
749                assert(paddr == (self.range.start + perm_idx * PAGE_SIZE) as usize);
750            }
751
752            let tracked_permission = unsafe {
753                #[verus_spec(with Tracked(regions))]
754                crate::mm::frame::inc_frame_ref_count(paddr)
755            };
756            let tracked frame_permission = tracked_permission.get();
757            proof {
758                let tracked slot_perm = regions.tracked_borrow_slot(paddr);
759                raw_perms.tracked_push(
760                    FrameRawPerms { slot_perm, metadata_perm: frame_permission },
761                );
762            }
763
764            paddr += PAGE_SIZE;
765
766            proof {
767                i = i + 1;
768            }
769        }
770
771        proof_with!{ tracked_perms: Tracked(Some(raw_perms)) }
772        Self { range: start..end, _marker: core::marker::PhantomData }
773    }
774
775    /// Forgets the [`Segment`] and gets a raw range of physical addresses.
776    /// # Verified Properties
777    /// ## Preconditions
778    /// - the segment must satisfy its invariant.
779    ///
780    /// ## Postconditions
781    /// - the returned physical address range matches the segment's range.
782    #[verus_spec(r =>
783        with
784            -> raw_perms: Tracked<Seq<FrameRawPerms>>,
785        requires
786            self.inv(),
787        ensures
788            r == self.range(),
789            raw_perms@ == self.raw_perms(),
790    )]
791    pub(crate) fn into_raw(mut self) -> Range<Paddr> {
792        let range = self.range.clone();
793
794        proof_decl!{
795            let tracked raw_perms = self.tracked_perms.tracked_take();
796        }
797
798        let _ = ManuallyDrop::new(self);
799
800        proof_with!(|= Tracked(raw_perms));
801        range
802    }
803
804    /// Splits the contiguous frames into two at the given byte offset from the start in spec mode.
805    pub closed spec fn split_spec(self, offset: usize) -> (Self, Self)
806        recommends
807            offset % PAGE_SIZE == 0,
808            0 < offset < self.size(),
809    {
810        let at = (self.start_paddr() + offset) as usize;
811        let idx = offset / PAGE_SIZE;
812        (
813            Self {
814                range: self.start_paddr()..at,
815                _marker: core::marker::PhantomData,
816                #[cfg(verus_keep_ghost_body)]
817                tracked_perms: Tracked(Some(self.raw_perms()[..idx])),
818            },
819            Self {
820                range: at..self.end_paddr(),
821                _marker: core::marker::PhantomData,
822                #[cfg(verus_keep_ghost_body)]
823                tracked_perms: Tracked(Some(self.raw_perms()[idx..])),
824            },
825        )
826    }
827}
828
829impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> FromSpecImpl<Frame<M>> for Segment<M> {
830    open spec fn obeys_from_spec() -> bool {
831        true
832    }
833
834    closed spec fn from_spec(frame: Frame<M>) -> Self {
835        let paddr = frame.start_paddr_spec();
836        let slot_perm = frame.slot_perm();
837        let metadata_perm = frame.frac_metadata_perm();
838        let perm =
839            seq!{
840            FrameRawPerms { slot_perm: &slot_perm, metadata_perm}
841        };
842        Self {
843            range: paddr..(paddr + PAGE_SIZE) as usize,
844            _marker: core::marker::PhantomData,
845            #[cfg(verus_keep_ghost_body)]
846            tracked_perms: Tracked(Some(perm)),
847        }
848    }
849}
850
851#[verus_verify]
852impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> From<Frame<M>> for Segment<M> {
853    fn from(frame: Frame<M>) -> Self {
854        assume(frame.inv());
855
856        let mut frame = frame;
857        let pa = frame.start_paddr();
858        proof_decl!{
859            let tracked frame_perm =
860                FrameRawPerms{
861                    slot_perm: *frame.tracked_slot_perm.borrow(),
862                    metadata_perm: frame.tracked_metadata_perm.tracked_take()
863                };
864            let tracked perms = Seq::tracked_empty();
865            perms.tracked_push(frame_perm);
866        }
867        let _ = ManuallyDrop::new(frame);
868        Self {
869            range: pa..(pa + PAGE_SIZE),
870            _marker: core::marker::PhantomData,
871            #[cfg(verus_keep_ghost_body)]
872            tracked_perms: Tracked(Some(perms)),
873        }
874    }
875}
876
877impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Iterator for Segment<M> {
878    type Item = Frame<M>;
879
880    #[verifier::rlimit(200)]
881    fn next(&mut self) -> Option<Self::Item> {
882        proof {
883            // This is a verification limitation that the `#[verifier::type_invariant]` can not be broken.
884            // It is still sound because `Segment` is always exposed with `inv`.
885            assume(self.inv());
886        }
887
888        if self.range.start < self.range.end {
889            proof {
890                assert(self.raw_perms()[0].slot_perm == self.slot_perms()[0]);
891                assert(self.raw_perms()[0].metadata_perm == self.metadata_perms()[0]);
892            }
893            let tracked mut raw_perms = self.tracked_perms.tracked_borrow_mut();
894            let tracked perm = raw_perms.tracked_pop_front();
895            proof {
896                assert(perm.inv());
897                assert(perm.slot_vaddr() == frame_to_meta(self.range.start));
898            }
899            // SAFETY: each frame in the range would be a handle forgotten
900            // when creating the `Segment` object.
901            let frame = unsafe {
902                #[verus_spec(with Tracked(perm))]
903                Frame::<M>::from_raw(self.range.start)
904            };
905            self.range.start += PAGE_SIZE;
906            Some(frame)
907        } else {
908            None
909        }
910    }
911}
912
913impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> IteratorSpecImpl for Segment<M> {
914    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
915        true
916    }
917
918    #[verifier::prophetic]
919    closed spec fn remaining(&self) -> Seq<Self::Item> {
920        Seq::new(
921            self.metadata_perms().len() as nat,
922            |i: int|
923                {
924                    Frame::<M>::from_raw_spec(
925                        (self.range().start + i * PAGE_SIZE) as usize,
926                        self.slot_perms()[i],
927                        Some(self.metadata_perms()[i]),
928                    )
929                },
930        )
931    }
932
933    #[verifier::prophetic]
934    closed spec fn will_return_none(&self) -> bool {
935        true
936    }
937
938    closed spec fn decrease(&self) -> Option<nat> {
939        Some(self.len() as nat)
940    }
941
942    open spec fn peek(&self, index: int) -> Option<Self::Item> {
943        if 0 <= index < self.metadata_perms().len() {
944            Some(
945                Frame::<M>::from_raw_spec(
946                    (self.range().start + index * PAGE_SIZE) as usize,
947                    self.slot_perms()[index],
948                    Some(self.metadata_perms()[index]),
949                ),
950            )
951        } else {
952            None
953        }
954    }
955}
956
957impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Segment<M> {
958    #[verus_spec(
959        with Tracked(regions): Tracked<&mut MetaRegionOwners>
960        requires
961            old(regions).inv(),
962            self.inv(),
963            self.relate_regions(*old(regions)),
964            forall|i: int|
965                #![trigger frame_to_index((self.start_paddr() + i * PAGE_SIZE) as usize)]
966                0 <= i < self.len() ==> {
967                    let idx = frame_to_index((self.start_paddr() + i * PAGE_SIZE) as usize);
968                    &&& old(regions).slot_owners[idx].storage_perm().is_init()
969                    &&& old(regions).ref_count(idx) == 1 ==> {
970                        &&& old(regions).slot_owners[idx].in_list_perm.value() == 0
971                    }
972                },
973        ensures
974            final(regions).inv(),
975    )]
976    pub fn drop(self) {
977        let ghost n = self.len();
978        let mut paddr = self.range.start;
979        let tracked mut raw_perms = self.tracked_perms.get().tracked_unwrap();
980
981        let ghost mut k: int = 0;
982
983        loop
984            invariant
985                old(regions).inv(),
986                regions.inv(),
987                self.inv(),
988                raw_perms.len() == n - k,
989                forall|j: int|
990                    #![trigger raw_perms[j]]
991                    0 <= j < raw_perms.len() ==> {
992                        let idx = frame_to_index((self.range.start + (k + j) * PAGE_SIZE) as usize);
993                        &&& raw_perms[j].inv()
994                        &&& raw_perms[j].slot_perm == regions.slots[idx]
995                        &&& raw_perms[j].metadata_perm.id()
996                            == regions.slot_owners[idx].metadata_perm.id()
997                    },
998                self.range.start <= paddr <= self.range.end,
999                paddr == (self.range.start + k * PAGE_SIZE) as usize,
1000                paddr % PAGE_SIZE == 0,
1001                paddr <= MAX_PADDR,
1002                0 <= k <= n,
1003                n == (self.range.end - self.range.start) / PAGE_SIZE as int,
1004                paddr < self.range.end <==> k < n,
1005                forall|j: int|
1006                    #![trigger frame_to_index((self.range.start + j * PAGE_SIZE) as usize)]
1007                    k <= j < n ==> {
1008                        let idx = frame_to_index((self.range.start + j * PAGE_SIZE) as usize);
1009                        &&& regions.contains(idx)
1010                        &&& regions.slot_owners[idx] == old(regions).slot_owners[idx]
1011                    },
1012                forall|j: int|
1013                    #![trigger frame_idx_at(self.range.start, j)]
1014                    k <= j < n ==> regions.contains(frame_idx_at(self.range.start, j))
1015                        && regions.slot_owners[frame_idx_at(self.range.start, j)] == old(
1016                        regions,
1017                    ).slot_owners[frame_idx_at(self.range.start, j)],
1018                regions.slot_owners.dom() == old(regions).slot_owners.dom(),
1019                self.relate_regions(*old(regions)),
1020                forall|i: int|
1021                    #![trigger frame_to_index((self.range.start + i * PAGE_SIZE) as usize)]
1022                    0 <= i < n ==> {
1023                        let idx = frame_to_index((self.range.start + i * PAGE_SIZE) as usize);
1024                        &&& old(regions).slot_owners[idx].storage_perm().is_init()
1025                        &&& old(regions).ref_count(idx) == 1 ==> {
1026                            &&& old(regions).slot_owners[idx].in_list_perm.value() == 0
1027                        }
1028                    },
1029            decreases n - k,
1030        {
1031            if paddr >= self.range.end {
1032                break;
1033            }
1034            let tracked perm = raw_perms.tracked_pop_front();
1035            let frame = unsafe {
1036                #[verus_spec(with Tracked(perm))]
1037                Frame::<M>::from_raw(paddr)
1038            };
1039
1040            frame.drop(Tracked(regions));
1041
1042            paddr += PAGE_SIZE;
1043
1044            proof {
1045                k = k + 1;
1046            }
1047        }
1048    }
1049}
1050
1051/*impl<M: AnyFrameMeta> TryFrom<Segment<dyn AnyFrameMeta>> for Segment<M> {
1052    type Error = Segment<dyn AnyFrameMeta>;
1053
1054    open spec fn clone_ensures(
1055        self,
1056        old_perm: MetaRegionOwners,
1057        new_perm: MetaRegionOwners,
1058        res: Self,
1059    ) -> bool {
1060        &&& res.range == self.range
1061        &&& res.inv()
1062        &&& new_perm.inv()
1063    }
1064
1065    fn clone(&self, Tracked(perm): Tracked<&mut MetaRegionOwners>) -> (res: Self) {
1066        let mut paddr = self.range.start;
1067
1068        let ghost old_perm = *perm;
1069        loop
1070            invariant
1071                perm.inv(),
1072                self.inv(),
1073                perm.slots == old_perm.slots,
1074                perm.slot_owners.dom() == old_perm.slot_owners.dom(),
1075                // Linear-drop pilot: cloning a Segment doesn't mint or
1076                // redeem its obligation — the per-frame ref-count bump is
1077                // an Arc-style operation.
1078                self.range.start <= paddr <= self.range.end,
1079                paddr % PAGE_SIZE == 0,
1080                paddr <= MAX_PADDR,
1081                forall|pa: Paddr|
1082                    #![trigger frame_to_index(pa)]
1083                    (paddr <= pa < self.range.end && pa % PAGE_SIZE == 0) ==> {
1084                        let idx = frame_to_index(pa);
1085                        &&& perm.contains(idx)
1086                        &&& valid_frame_paddr(pa)
1087                        &&& perm.ref_count(idx) > 0
1088                        &&& perm.ref_count(idx) + 1
1089                            < REF_COUNT_MAX
1090                        &&& !MetaSlot::inc_ref_count_panic_cond(
1091                            perm.slot_owners[idx].ref_count_perm,
1092                        )
1093                    },
1094            decreases self.range.end - paddr,
1095        {
1096            if paddr >= self.range.end {
1097                break;
1098            }
1099            #[verus_spec(with Tracked(perm))]
1100            crate::mm::frame::inc_frame_ref_count(paddr);
1101
1102            paddr = paddr + PAGE_SIZE;
1103        }
1104        // Since segments are homogeneous, we can safely assume that the rest
1105        // of the frames are of the same type. We just debug-check here.
1106        #[cfg(debug_assertions)]
1107        {
1108            for paddr in seg.range.clone().step_by(PAGE_SIZE) {
1109                let frame = unsafe { Frame::<dyn AnyFrameMeta>::from_raw(paddr) };
1110                let frame = ManuallyDrop::new(frame);
1111                debug_assert!((frame.dyn_meta() as &dyn core::any::Any).is::<M>());
1112            }
1113        }
1114        // SAFETY: The metadata is coerceable and the struct is transmutable.
1115        Ok(unsafe { core::mem::transmute::<Segment<dyn AnyFrameMeta>, Segment<M>>(seg) })
1116    }
1117}
1118
1119impl<M: AnyUFrameMeta> From<Segment<M>> for USegment {
1120    fn from(seg: Segment<M>) -> Self {
1121        // SAFETY: The metadata is coerceable and the struct is transmutable.
1122        unsafe { core::mem::transmute(seg) }
1123    }
1124}
1125
1126impl TryFrom<Segment<dyn AnyFrameMeta>> for USegment {
1127    type Error = Segment<dyn AnyFrameMeta>;
1128
1129    /// Try converting a [`Segment<dyn AnyFrameMeta>`] into [`USegment`].
1130    ///
1131    /// If the usage of the page is not the same as the expected usage, it will
1132    /// return the dynamic page itself as is.
1133    fn try_from(seg: Segment<dyn AnyFrameMeta>) -> core::result::Result<Self, Self::Error> {
1134        // SAFETY: for each page there would be a forgotten handle
1135        // when creating the `Segment` object.
1136        let first_frame = unsafe { Frame::<dyn AnyFrameMeta>::from_raw(seg.range.start) };
1137        let first_frame = ManuallyDrop::new(first_frame);
1138        if !first_frame.dyn_meta().is_untyped() {
1139            return Err(seg);
1140        }
1141        // Since segments are homogeneous, we can safely assume that the rest
1142        // of the frames are of the same type. We just debug-check here.
1143        #[cfg(debug_assertions)]
1144        {
1145            for paddr in seg.range.clone().step_by(PAGE_SIZE) {
1146                let frame = unsafe { Frame::<dyn AnyFrameMeta>::from_raw(paddr) };
1147                let frame = ManuallyDrop::new(frame);
1148                debug_assert!(frame.dyn_meta().is_untyped());
1149            }
1150        }
1151        // SAFETY: The metadata is coerceable and the struct is transmutable.
1152        Ok(unsafe { core::mem::transmute::<Segment<dyn AnyFrameMeta>, USegment>(seg) })
1153    }
1154} */
1155
1156impl<M: AnyFrameMeta + ?Sized> Inv for Segment<M> {
1157    /// The invariant of a [`Segment`]:
1158    ///
1159    /// - the physical addresses of the frames are aligned and within bounds.
1160    /// - the range is well-formed, i.e., the start is less than or equal to the end.
1161    open spec fn inv(self) -> bool {
1162        &&& self.start_paddr() % PAGE_SIZE == 0
1163        &&& self.end_paddr() % PAGE_SIZE == 0
1164        &&& self.start_paddr() <= self.end_paddr() <= MAX_PADDR
1165        &&& self.inner_perm_inv()
1166        &&& self.raw_perms().len() == self.len()
1167        &&& forall|i: int|
1168            #![trigger self.raw_perms()[i]]
1169            0 <= i < self.raw_perms().len() ==> {
1170                let paddr = (self.range().start + i * PAGE_SIZE) as usize;
1171                &&& self.raw_perms()[i].slot_vaddr() == frame_to_meta(paddr)
1172                &&& self.raw_perms()[i].inv()
1173            }
1174    }
1175}
1176
1177} // verus!
ostd/mm/frame/segment.rs

ostd/mm/frame/
segment.rs
