Skip to content

std.io

Files and standard streams. A File is linear: the type system, not a convention, is what closes a descriptor, and defer close(f) is the one idiom that survives an early try. Errors are errno in an IoError, because CAIRN cannot express int* and the C library keeps its error behind one. Cost: one syscall per call except write, read_full and the _to_end reads, which loop until the kernel is done; nothing here buffers, so n bytes written is n bytes of syscall.

pub struct IoError { code:i32; }
pub linear struct File { fd:i32; }

// open flags and lseek origins, exactly as Linux defines them.
pub const READ:i32 = 0;

pub const WRITE:i32 = 66;
pub const APPEND:i32 = 1090;
pub const TRUNCATE:i32 = 578;
pub const SET:i32 = 0;
pub const CUR:i32 = 1;
pub const END:i32 = 2;

// `path` must end in a NUL byte, since C reads a pointer and not a length.
// effects: ffi:__errno_location, ffi:open, ffi_precondition, io, mmio, read:path, trap
pub fn open(n:usize, path:ro<u8>[n]@host, flags:i32) -> std.core.Result[std.io.File, std.io.IoError]

// The consumer of the linear value. It cannot report a status: a function that returns one has a `return` statement,
// and a `return` demands that every linear value be consumed first.
pub fn close(f:std.io.File)  // effects: ffi:close, io

// effects: ffi:__errno_location, ffi:read, ffi_precondition, io, mmio, read:f, trap, write:into
pub fn read(f:ro<std.io.File>, n:usize, into:rw<u8>[n]@host) -> std.core.Result[usize, std.io.IoError]

// Fills `into` unless the file ends first; the returned count says which happened.
// effects: diverge, ffi:__errno_location, ffi:read, ffi_precondition, io, mmio, read:f, trap, write:into
pub fn read_full(f:ro<std.io.File>, n:usize, into:rw<u8>[n]@host) -> std.core.Result[usize, std.io.IoError]

// A short write is not an error to the kernel; it is here, so callers never lose a tail.
// effects: diverge, ffi:__errno_location, ffi:write, ffi_precondition, io, mmio, read:data, read:f, trap
pub fn write(f:ro<std.io.File>, n:usize, data:ro<u8>[n]@host) -> std.core.Result[usize, std.io.IoError]

// effects: ffi:__errno_location, ffi:lseek, io, mmio, read:f, trap
pub fn seek(f:ro<std.io.File>, offset:i64, whence:i32) -> std.core.Result[u64, std.io.IoError]

// effects: ffi:__errno_location, ffi:lseek, io, mmio, read:f, trap
pub fn size(f:ro<std.io.File>) -> std.core.Result[u64, std.io.IoError]

// Durability is a syscall, never a side effect of closing.
// effects: ffi:__errno_location, ffi:fsync, io, mmio, read:f, trap
pub fn sync(f:ro<std.io.File>) -> std.core.Result[usize, std.io.IoError]

// Cut a torn tail off a log: the offset becomes the new end of file.
// effects: ffi:__errno_location, ffi:ftruncate, io, mmio, read:f, trap
pub fn truncate(f:ro<std.io.File>, length:u64) -> std.core.Result[usize, std.io.IoError]

// effects: ffi:__errno_location, ffi:unlink, ffi_precondition, io, mmio, read:path, trap
pub fn remove(n:usize, path:ro<u8>[n]@host) -> std.core.Result[usize, std.io.IoError]

// One atomic replacement, which is how a compacted file becomes the live one.
// effects: ffi:__errno_location, ffi:rename, ffi_precondition, io, mmio, read:from, read:to, trap
pub fn rename(n:usize, from:ro<u8>[n]@host, m:usize, to:ro<u8>[m]@host) -> std.core.Result[usize, std.io.IoError]

// Everything left to read, however it arrives: a pipe, a socket, /proc, a file whose size lies. Each read fills the
// room `into` has spare, and a full `into` doubles; the count is what was added. Cost: after the first read, `f` is
// asked how much is left, so the rest of a regular file arrives in one allocation; a pipe's `into` doubles as it fills.
// A read that fails first, such as a directory's (EISDIR, 21), is returned before any size is asked, since ext4 gives a
// directory's end as 2^63 - 1.
// effects: alloc, diverge, ffi:__errno_location, ffi:lseek, ffi:read, ffi_precondition, free, io, local_read,
// local_write, mmio, read:f, read:into, trap, write:into, zero_init
pub fn read_to_end(f:ro<std.io.File>, into:rw<std.vec.Vec[u8]>) -> std.core.Result[usize, std.io.IoError]

// The whole file, sized once and read in one pass; the Vec is exactly as large as the file.
// effects: alloc, diverge, ffi:__errno_location, ffi:close, ffi:lseek, ffi:open, ffi:read, ffi_precondition, free, io,
// local_read, local_write, mmio, read:path, trap, zero_init
pub fn read_file(n:usize, path:ro<u8>[n]@host) -> std.core.Result[std.vec.Vec[u8], std.io.IoError]

pub fn print(n:usize, data:ro<u8>[n]@host)  // effects: diverge, ffi:write, ffi_precondition, io, read:data, trap
pub fn println(n:usize, data:ro<u8>[n]@host)  // effects: diverge, ffi:write, ffi_precondition, io, read:data, trap
pub fn eprintln(n:usize, data:ro<u8>[n]@host)  // effects: diverge, ffi:write, ffi_precondition, io, read:data, trap
pub fn newline()  // effects: diverge, ffi:write, ffi_precondition, io, trap

// effects: diverge, ffi:write, ffi_precondition, io, local_read, local_write, stack_storage, trap, zero_init
pub fn print_u64(value:u64)

// effects: diverge, ffi:write, ffi_precondition, io, local_read, local_write, stack_storage, trap, zero_init
pub fn print_i64(value:i64)

// All of standard input from where it stands, appended to `into` as read_to_end appends a file's; the count is what was
// added, and standard input stays open. Cost: after the first read, the rest of input redirected from a file arrives in
// one allocation, and a pipe's `into` doubles as it fills.
// effects: alloc, diverge, ffi:__errno_location, ffi:lseek, ffi:read, ffi_precondition, free, io, local_read,
// local_write, mmio, read:into, trap, write:into, zero_init
pub fn read_stdin_to_end(into:rw<std.vec.Vec[u8]>) -> std.core.Result[usize, std.io.IoError]

// One read from standard input: 0 at end of input, as `read` answers for a file.
// effects: ffi:__errno_location, ffi:read, ffi_precondition, io, mmio, trap, write:into
pub fn read_stdin(n:usize, into:rw<u8>[n]@host) -> std.core.Result[usize, std.io.IoError]

// CLOCK_MONOTONIC in nanoseconds: the only clock a measurement should trust.
// effects: ffi:clock_gettime, ffi_precondition, io, local_read, local_write, stack_storage, trap, zero_init
pub fn monotonic_ns() -> u64

// What an I/O ring's `q.next(tag, result)` reported: a byte count or a new descriptor, or the error the kernel gave,
// which a ring returns as a negative errno instead of setting errno.
pub fn outcome(result:i64) -> std.core.Result[usize, std.io.IoError]  // effects: trap

A generic function's effects are what it may do for any arguments within its bounds, besides what their own trait members do.