Function wasi_args_get

src/wrappers.rs:902–942

#[ensures(effects!(old(trace), trace))]

(ctx: &mut VmCtx, argv: u32, argv_buf: u32)

#[ensures(trace_safe(trace, ctx))]
// #[ensures(effects!(old(trace), trace))]
pub fn wasi_args_get(ctx: &mut VmCtx, argv: u32, argv_buf: u32) -> RuntimeResult<()> {
    // 1. copy argv_buffer
    let argv_buf_len = ctx.arg_buffer.len() as u32;
    ctx.copy_arg_buffer_to_sandbox(argv_buf, argv_buf_len)?;
    // 2. copy in argv
    let mut idx: usize = 0;
    let mut start: u32 = 0;
    let mut cursor: usize = 0;
    while idx < ctx.arg_buffer.len() {
        body_invariant!(ctx_safe(ctx));
        body_invariant!(trace_safe(trace, ctx));
        // We have found an argument either when we find a trailing space, or if we started an arg
        // and ran out of space
        if !ctx.fits_in_lin_mem_usize((argv as usize) + cursor, 8) {
            return Err(Eoverflow);
        }

        if ctx.arg_buffer[idx] == b'\0' {
            while idx < ctx.arg_buffer.len() && ctx.arg_buffer[idx] == b'\0' {
                idx += 1;
            } // scan past multiple spaces
            ctx.write_u32((argv as usize) + cursor, argv_buf + start);
            cursor += 4;
            start = idx as u32;
        }
        idx += 1;

        // we reached the end, so record the final arg
        if idx >= ctx.arg_buffer.len() {
            ctx.write_u32((argv as usize) + cursor, argv_buf + start);
        }
    }

    let argc = ctx.argc;
    // ensure the last entry is null
    if !ctx.fits_in_lin_mem_usize((argv as usize) + argc * 4, 8) {
        return Err(Eoverflow);
    }
    ctx.write_u32((argv as usize) + argc * 4, 0);
    Ok(())
}

// https://github.com/WebAssembly/WASI/blob/main/phases/snapshot/docs.md#environ_get
#[with_ghost_var(trace: &mut Trace)]