Function wasi_path_open

src/wrappers.rs:38–72

(
    ctx: &mut VmCtx,
    v_dir_fd: u32,
    dirflags: u32,
    pathname: u32,
    path_len: u32,
    oflags: u32,
    fdflags: i32,
)

#[ensures(ctx_safe(ctx))]
#[ensures(trace_safe(trace, ctx))]
pub fn wasi_path_open(
    ctx: &mut VmCtx,
    v_dir_fd: u32,
    dirflags: u32,
    pathname: u32,
    path_len: u32,
    oflags: u32,
    fdflags: i32,
) -> RuntimeResult<u32> {
    let dirflags = LookupFlags::new(dirflags);
    let oflags = OFlags::new(oflags);
    let fdflags = FdFlags::from(fdflags);
    let should_follow = dirflags.should_follow();

    if v_dir_fd != HOMEDIR_FD {
        return Err(Enotcapable);
    }
    let fd = ctx.homedir_host_fd;

    let host_pathname = ctx.translate_path(pathname, path_len, should_follow, fd);
    unwrap_result!(host_pathname);

    let dflags = dirflags.to_openat_posix();
    let flags = bitwise_or(bitwise_or(dflags, oflags.to_posix()), fdflags.to_posix());

    if flag_set(flags, libc::O_NOFOLLOW) == should_follow {
        // this should never happen, but adding an extra dynamic check let me
        // avoid reasoning about bitwise operation math (which prusti does not support well)
        // in the proof
        return Err(Einval);
    }

    let fd = trace_openat(ctx, fd, host_pathname, flags)?;
    ctx.fdmap.create(HostFd::from_raw(fd))
}

// https://github.com/WebAssembly/WASI/blob/main/phases/snapshot/docs.md#fd_close
// modifies: fdmap