Function wasi_path_link

src/wrappers.rs:569–622

(
    ctx: &VmCtx,
    v_old_fd: u32,
    flags: u32,
    old_pathname: u32,
    old_path_len: u32,
    v_new_fd: u32,
    new_pathname: u32,
    new_path_len: u32,
)

#[ensures(ctx_safe(ctx))]
#[ensures(trace_safe(trace, ctx))]
pub fn wasi_path_link(
    ctx: &VmCtx,
    v_old_fd: u32,
    flags: u32,
    old_pathname: u32,
    old_path_len: u32,
    v_new_fd: u32,
    new_pathname: u32,
    new_path_len: u32,
) -> RuntimeResult<()> {
    let flags = LookupFlags::new(flags);

    // let old_fd = ctx.fdmap.fd_to_native(v_old_fd)?;
    // let new_fd = ctx.fdmap.fd_to_native(v_new_fd)?;

    if v_old_fd != HOMEDIR_FD {
        return Err(Enotcapable);
    }
    assert!(v_old_fd == HOMEDIR_FD);
    let old_fd = ctx.homedir_host_fd;

    if v_new_fd != HOMEDIR_FD {
        return Err(Enotcapable);
    }
    assert!(v_new_fd == HOMEDIR_FD);
    let new_fd = ctx.homedir_host_fd;

    let should_follow = flags.should_follow();

    // when resolveing paths for path_link, we resolve the final symlink
    let old_host_pathname = ctx.translate_path(old_pathname, old_path_len, should_follow, old_fd);
    unwrap_result!(old_host_pathname);
    let new_host_pathname = ctx.translate_path(new_pathname, new_path_len, should_follow, new_fd);
    unwrap_result!(new_host_pathname);

    let n_flags = flags.to_linkat_posix();

    if flag_set(n_flags, libc::AT_SYMLINK_FOLLOW) != 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 res = trace_linkat(
        ctx,
        old_fd,
        old_host_pathname,
        new_fd,
        new_host_pathname,
        n_flags,
    )?;
    Ok(())
}

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