ostd::mm::io

Struct Fallible

pub struct Fallible {}

Expand description

Marker type indicating that VM I/O operations may fail (e.g., user-space access).

Trait Implementations§

Source §

impl<'a> FallibleVmRead<Fallible> for VmReader<'a, Fallible>

Source §

exec fn read_fallible( &mut self, writer: &mut VmWriter<'_, Fallible>, ) -> r : Result<usize, (Error, usize)>

requires

old(self).inv(),

old(writer).inv(),

ensures

final(self).end == old(self).end,

final(self).id == old(self).id,

final(self).cursor.range == old(self).cursor.range,

final(writer).end == old(writer).end,

final(writer).id == old(writer).id,

final(writer).cursor.range == old(writer).cursor.range,

final(self).inv(),

final(writer).inv(),

match r {
    Ok(n) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + n
        &&& final(writer).cursor.vaddr == old(writer).cursor.vaddr + n
        &&& n <= old(self).remain_spec()
        &&& n <= old(writer).avail_spec()

    ),
    Err((_, copied_len)) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + copied_len
        &&& final(writer).cursor.vaddr == old(writer).cursor.vaddr + copied_len
        &&& copied_len <= old(self).remain_spec()
        &&& copied_len <= old(writer).avail_spec()

    ),
},

Source §

impl<'a> FallibleVmRead<Fallible> for VmReader<'a, Infallible>

Source §

exec fn read_fallible( &mut self, writer: &mut VmWriter<'_, Fallible>, ) -> r : Result<usize, (Error, usize)>

requires

old(self).inv(),

old(writer).inv(),

ensures

final(self).end == old(self).end,

final(self).id == old(self).id,

final(self).cursor.range == old(self).cursor.range,

final(writer).end == old(writer).end,

final(writer).id == old(writer).id,

final(writer).cursor.range == old(writer).cursor.range,

final(self).inv(),

final(writer).inv(),

match r {
    Ok(n) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + n
        &&& final(writer).cursor.vaddr == old(writer).cursor.vaddr + n
        &&& n <= old(self).remain_spec()
        &&& n <= old(writer).avail_spec()

    ),
    Err((_, copied_len)) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + copied_len
        &&& final(writer).cursor.vaddr == old(writer).cursor.vaddr + copied_len
        &&& copied_len <= old(self).remain_spec()
        &&& copied_len <= old(writer).avail_spec()

    ),
},

Source §

impl<'a> FallibleVmWrite<Fallible> for VmWriter<'a, Fallible>

Source §

exec fn write_fallible( &mut self, reader: &mut VmReader<'_, Fallible>, ) -> r : Result<usize, (Error, usize)>

requires

old(self).inv(),

old(reader).inv(),

ensures

final(self).end == old(self).end,

final(self).id == old(self).id,

final(self).cursor.range == old(self).cursor.range,

final(reader).end == old(reader).end,

final(reader).id == old(reader).id,

final(reader).cursor.range == old(reader).cursor.range,

final(self).inv(),

final(reader).inv(),

match r {
    Ok(n) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + n
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + n
        &&& n <= old(self).avail_spec()
        &&& n <= old(reader).remain_spec()

    ),
    Err((_, copied_len)) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + copied_len
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + copied_len
        &&& copied_len <= old(self).avail_spec()
        &&& copied_len <= old(reader).remain_spec()

    ),
},

Source §

impl<'a> FallibleVmWrite<Fallible> for VmWriter<'a, Infallible>

Source §

exec fn write_fallible( &mut self, reader: &mut VmReader<'_, Fallible>, ) -> r : Result<usize, (Error, usize)>

requires

old(self).inv(),

old(reader).inv(),

ensures

final(self).end == old(self).end,

final(self).id == old(self).id,

final(self).cursor.range == old(self).cursor.range,

final(reader).end == old(reader).end,

final(reader).id == old(reader).id,

final(reader).cursor.range == old(reader).cursor.range,

final(self).inv(),

final(reader).inv(),

match r {
    Ok(n) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + n
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + n
        &&& n <= old(self).avail_spec()
        &&& n <= old(reader).remain_spec()

    ),
    Err((_, copied_len)) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + copied_len
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + copied_len
        &&& copied_len <= old(self).avail_spec()
        &&& copied_len <= old(reader).remain_spec()

    ),
},