Use Verus-verified page table for aarch64 #201
Conversation
There was a problem hiding this comment.
Pull Request Overview
This PR replaces the existing page table implementation with a Verus-verified version for aarch64 architecture. The change improves code reliability by using formal verification while maintaining the same API interface.
- Removes custom page table entry (PTE) implementation and related attribute handling
- Integrates hvisor-pt library with Verus verification support
- Updates page table operations to use the new verified implementation
Reviewed Changes
Copilot reviewed 3 out of 4 changed files in this pull request and generated 4 comments.
| File | Description |
|---|---|
| src/arch/aarch64/s2pt.rs | Removes custom PageTableEntry and descriptor attribute implementations, simplifies type definition |
| src/arch/aarch64/paging.rs | Replaces custom page table with Aarch64PageTable from hvisor-pt, adds Verus integration |
| Cargo.toml | Adds dependencies for vstd and hvisor-pt libraries |
Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.
| spec fn view(self) -> PageTableMem { | ||
| PageTableMem { | ||
| tables: Seq::new(self.tables.len() as nat, |i| Table { | ||
| base: self.frames[i].start_paddr(), |
There was a problem hiding this comment.
Field access self.frames[i] should be self.tables[i] to match the struct field name defined on line 155.
| base: self.frames[i].start_paddr(), | |
| base: self.tables[i].start_paddr(), |
| fn read(&self, base:PAddrExec, index:usize) -> u64 { | ||
| unsafe { (base.0 as *const u64).offset(index as isize).read_volatile() } | ||
| } | ||
|
|
||
| fn unmap_page(&mut self, vaddr: VA) -> PagingResult<(PhysAddr, PageSize)> { | ||
| let (entry, size) = self.inner.get_entry_mut(vaddr)?; | ||
| if entry.is_unused() { | ||
| return Err(PagingError::NotMapped); | ||
| } | ||
| let paddr = entry.addr(); | ||
| entry.clear(); | ||
| Ok((paddr, size)) | ||
| fn write(&mut self, base:PAddrExec, index:usize, val:u64) { |
There was a problem hiding this comment.
[nitpick] Missing spaces after colons in parameter declarations. Should be base: PAddrExec, index: usize for consistency with Rust formatting conventions.
| fn read(&self, base:PAddrExec, index:usize) -> u64 { | ||
| unsafe { (base.0 as *const u64).offset(index as isize).read_volatile() } | ||
| } | ||
|
|
||
| fn unmap_page(&mut self, vaddr: VA) -> PagingResult<(PhysAddr, PageSize)> { | ||
| let (entry, size) = self.inner.get_entry_mut(vaddr)?; | ||
| if entry.is_unused() { | ||
| return Err(PagingError::NotMapped); | ||
| } | ||
| let paddr = entry.addr(); | ||
| entry.clear(); | ||
| Ok((paddr, size)) | ||
| fn write(&mut self, base:PAddrExec, index:usize, val:u64) { |
There was a problem hiding this comment.
[nitpick] Missing spaces after colons in parameter declarations. Should be base: PAddrExec, index: usize for consistency with Rust formatting conventions.
| }; | ||
| Self { | ||
| inner: HvPageTableUnlocked::new(level), | ||
| inner: Aarch64PageTable::new(arch, 0x0, 0x80000000), |
There was a problem hiding this comment.
[nitpick] Magic numbers 0x0 and 0x80000000 should be defined as named constants to improve code readability and maintainability.
Features
src/arch/aarch64/paging.rs).