Skip to content

Commit 509d6d2

Browse files
authored
Merge pull request #55 from PLSysSec/result_fix_2
adjust tock so that flux-core Result spec doesn't break it
2 parents f3b09aa + 04d5058 commit 509d6d2

3 files changed

Lines changed: 14 additions & 0 deletions

File tree

arch/rv32i/src/pmp.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1300,6 +1300,7 @@ impl<const MAX_REGIONS: usize, P: TORUserPMP<MAX_REGIONS> + 'static> kernel::pla
13001300
// type MpuConfig = PMPUserMPUConfig<MAX_REGIONS>;
13011301
type Region = PMPUserRegion<MAX_REGIONS>;
13021302

1303+
#[flux_rs::trusted]
13031304
fn enable_app_mpu(&self) -> MpuEnabledCapability {
13041305
// TODO: This operation may fail when the PMP is not exclusively used
13051306
// for userspace. Instead of panicing, we should handle this case more
@@ -1360,6 +1361,8 @@ pub mod test {
13601361
Ok(())
13611362
}
13621363

1364+
// #[flux_rs::sig(fn (x: usize) -> u32[x] requires x <= u32::MAX)]
1365+
#[flux_rs::sig(fn (&Self) -> Result<(), ()>[true])]
13631366
fn enable_user_pmp(&self) -> Result<(), ()> {
13641367
Ok(())
13651368
} // The kernel's MPU trait requires

flux_support/src/extern_specs/result.rs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,4 +14,14 @@ impl<T, E> Result<T, E> {
1414

1515
#[sig(fn(&Result<T,E>[@b]) -> bool[!b])]
1616
const fn is_err(&self) -> bool;
17+
18+
#[sig(fn(Result<T, E>[true]) -> T)]
19+
fn unwrap(self) -> T
20+
where
21+
E: core::fmt::Debug;
22+
23+
#[sig(fn(Result<T, E>[false]) -> E)]
24+
fn unwrap_err(self) -> E
25+
where
26+
T: core::fmt::Debug;
1727
}

kernel/src/syscall_driver.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,7 @@ impl CommandReturn {
8181
}
8282

8383
impl From<Result<(), ErrorCode>> for CommandReturn {
84+
#[flux_rs::trusted]
8485
fn from(rc: Result<(), ErrorCode>) -> Self {
8586
match rc {
8687
Ok(()) => CommandReturn::success(),

0 commit comments

Comments
 (0)