Function parse_subscriptions

src/poll.rs:101–152

#[external_calls(poll_handle_fds, poll_handle_clock)]

(
    ctx: &VmCtx,
    in_ptr: u32,
    nsubscriptions: u32,
    precision: u64,
    min_timeout: &mut Option<Timestamp>,
    timeouts: &mut Vec<(u64, Timestamp)>,
    pollfds: &mut Vec<libc::pollfd>,

#[ensures(trace_safe(trace, ctx))]
// #[external_calls(poll_handle_fds, poll_handle_clock)]
pub fn parse_subscriptions(
    ctx: &VmCtx,
    in_ptr: u32,
    nsubscriptions: u32,
    precision: u64,
    min_timeout: &mut Option<Timestamp>,
    timeouts: &mut Vec<(u64, Timestamp)>,
    pollfds: &mut Vec<libc::pollfd>,
    fd_data: &mut Vec<(u64, SubscriptionFdType)>,
) -> RuntimeResult<()> {
    let mut i = 0;
    while i < nsubscriptions {
        body_invariant!(ctx_safe(ctx));
        body_invariant!(trace_safe(trace, ctx));

        let sub_offset = i * Subscription::WASI_SIZE;

        if !ctx.fits_in_lin_mem_usize(
            (in_ptr + sub_offset) as usize,
            Subscription::WASI_SIZE as usize,
        ) {
            return Err(Eoverflow);
        }

        let subscription = Subscription::read(ctx, in_ptr + sub_offset)?;

        match subscription.subscription_u {
            SubscriptionInner::Clock(subscription_clock) => {
                poll_parse_clock(
                    ctx,
                    subscription_clock,
                    precision,
                    min_timeout,
                    timeouts,
                    subscription.userdata,
                )?;
            }
            SubscriptionInner::Fd(subscription_readwrite) => {
                poll_parse_fds(
                    ctx,
                    pollfds,
                    fd_data,
                    subscription.userdata,
                    subscription_readwrite,
                )?;
            }
        }

        i += 1;
    }
    Ok(())
}

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