Function writeback_timeouts

src/poll.rs:159–193

(
    ctx: &mut VmCtx,
    out_ptr: u32,
    timeouts: &Vec<(u64, Timestamp)>,
    min_timeout: &Option<Timestamp>,
)

#[ensures(ctx_safe(ctx))]
#[ensures(trace_safe(trace, ctx))]
pub fn writeback_timeouts(
    ctx: &mut VmCtx,
    out_ptr: u32,
    timeouts: &Vec<(u64, Timestamp)>,
    min_timeout: &Option<Timestamp>,
) -> RuntimeResult<u32> {
    let mut num_events_written = 0;
    let mut event_idx = 0;
    while event_idx < timeouts.len() {
        body_invariant!(ctx_safe(ctx));
        body_invariant!(trace_safe(trace, ctx));

        let (userdata, timeout) = timeouts[event_idx];
        let event_offset = (num_events_written * Event::WASI_SIZE) as usize;
        if !ctx.fits_in_lin_mem_usize(out_ptr as usize + event_offset, Event::WASI_SIZE as usize) {
            return Err(Eoverflow);
        }
        // Technically we know there must be a min_timeout, but use if let to be safe
        if let Some(m_timeout) = min_timeout {
            if timeout == *m_timeout {
                let event = Event {
                    userdata,
                    error: RuntimeError::Success,
                    typ: EventType::Clock,
                    fd_readwrite: None,
                };
                event.write(ctx, out_ptr + event_offset as u32);
                num_events_written += 1;
            }
        }
        event_idx += 1;
    }

    return Ok(num_events_written);
}

#[with_ghost_var(trace: &mut Trace)]
#[requires(ctx_safe(ctx))]