diff --git a/bend2/base.bend b/bend2/base.bend index d7d118e546..7e8a184108 100644 --- a/bend2/base.bend +++ b/bend2/base.bend @@ -301,6 +301,14 @@ def File.read_at(file: File, offset: U32, max: U32) -> import "./effs/file_read.c" import "./effs/file_read.js" +# Reads up to max bytes at offset straight into a's U32 slots from at on, +# little-endian, four bytes a slot, with no List between: the count read, +# or the error. It stops at a's end; a stays a's size and owner. +def File.read_into(file: File, offset: U32, max: U32, a: Array, at: U32) -> + IO(File & (Array & Result<&1, &1, U32 & String, U32>)): + import "./effs/file_read.c" + import "./effs/file_read.js" + def File.size(file: File) -> IO(File & Result<&1, &1, U32 & String, U32>): import "./effs/file_size.c" diff --git a/bend2/effs/file_read.c b/bend2/effs/file_read.c index f7b8f564ed..e663304be7 100644 --- a/bend2/effs/file_read.c +++ b/bend2/effs/file_read.c @@ -73,3 +73,51 @@ static void __attribute__((constructor)) file_read_at_use(void) { } #endif + +#ifdef CID(File.read_into) + +// An Array block packs its slots little-endian, two to a 64-bit word, +// so slot i is byte 4i of the block: the bytes land there as the file holds +// them, with no List between. A forked handle writes the shared cells, as +// Array.set does. On a GPU the block is already in the device's buffer. +static void file_read_into_call(IoWork* w) { + u64 got = 0; + while (got < w->word) { + u64 want = w->word - got; + ssize_t n = pread((int)w->hand, w->data + got, + want < (1u << 30) ? want : (1u << 30), (off_t)w->made + (off_t)got); + if (n <= 0) { + if (n < 0) { + io_sys_end(w, n); + } + break; + } + got += (u64)n; + } + w->size = got; +} + +static Term file_read_into_pack(Env e, IoWork* w) { + Term r = io_res(e, w, w->size); + return io_tup(e, io_hand(w->hand), io_tup(e, w->item, r)); +} + +Term file_read_into_run(Env e, Term* f, IoWork* w) { + Term a = f[3]; + u64 at = (u32)f[4]; + u64 n = 1ull << blk_cls(a); + u64 room = at < n ? (n - at) * 4 : 0; + w->hand = (intptr_t)io_hand_v(f[0]); + w->made = (intptr_t)(u32)f[1]; + w->word = (u32)f[2] < room ? (u32)f[2] : (u32)room; + w->item = a; + w->code = 0; + w->data = (char*)&e.mem[blk_loc(e.mem, a)] + at * 4; + return io_work(w, file_read_into_call, file_read_into_pack); +} + +static void __attribute__((constructor)) file_read_into_use(void) { + io_eff(CID(File.read_into), file_read_into_run); +} + +#endif diff --git a/bend2/effs/file_read.js b/bend2/effs/file_read.js index 812bcaeea9..d7d2d0fe54 100644 --- a/bend2/effs/file_read.js +++ b/bend2/effs/file_read.js @@ -25,3 +25,43 @@ function file_read_at(file, offset, max) { io_eff(CID(File.read), file_read); io_eff(CID(File.read_bytes), file_read_bytes); io_eff(CID(File.read_at), file_read_at); + +// Slot at + i/4 takes bytes i..i+3 little-endian; a last partial slot +// keeps its high bytes, as the C block does. It reads in bounded chunks, +// so a large array with a small file allocates only what it reads. +function file_read_byte(a, at, i, x) { + const s = at + (i >>> 2), k = (i & 3) * 8; + a[s] = ((a[s] & ~(0xff << k)) | (x << k)) >>> 0; +} + +function file_read_into(file, offset, max, a, at) { + const sys = io_sys(); + const len = Math.max(0, Math.min(max, (a.length - at) * 4)); + const b = new Uint8Array(Math.max(Math.min(len, 1 << 24), 1)); + let got = 0; + while (got < len) { + const n = Number(sys.pread(file, sys.ptr(b), Math.min(len - got, b.length), + BigInt(offset + got))); + if (n < 0) { + return io_tup(file, io_tup(a, io_fail(sys.errno()))); + } + let i = 0; + for (; i < n && ((got + i) & 3) !== 0; i += 1) { + file_read_byte(a, at, got + i, b[i]); + } + for (; i + 4 <= n; i += 4) { + a[at + ((got + i) >>> 2)] = + (b[i] | (b[i + 1] << 8) | (b[i + 2] << 16) | (b[i + 3] << 24)) >>> 0; + } + for (; i < n; i += 1) { + file_read_byte(a, at, got + i, b[i]); + } + if (n === 0) { + break; + } + got += n; + } + return io_tup(file, io_tup(a, io_done(got))); +} + +io_eff(CID(File.read_into), file_read_into); diff --git a/tests/io/file_read_into.bend b/tests/io/file_read_into.bend new file mode 100644 index 0000000000..8fac691eae --- /dev/null +++ b/tests/io/file_read_into.bend @@ -0,0 +1,209 @@ +# File.read_into lands bytes little-endian in an Array's own slots: a +# short tail keeps its slot's high bytes, a read stops at the array's end and +# at the file's, and a failed read keeps the handle and the array and leaves +# no error behind for the next read. +import Base + +law bytes: + for n: Nat + for +at: U32 + List<&2, U32> + +def bytes(n, at): + match n: + case 0n: Nil{} + case 1n+p: at <> bytes(p, U32.add(at, 1)) + +law check: + for name: String + for ok: Bool + IO(Unit) + +def check(name, ok): + match ok: + case True{}: IO.print(name) + case False{}: IO.die(Unit, 1, "FAIL " ++ name) + +law wrote: + for pair: File & Result<&1, &1, U32 & String, Unit> + IO(Unit) + +def wrote(pair): + (file, result) = pair + do IO: + IO.pass(Unit, result) + File.close(file) + +law write: + IO(Unit) + +def write(): + do IO: + f : File <- IO.try(File, File.open("/tmp/bend_io_file_read_into", "w")) + p : File & Result<&1, &1, U32 & String, Unit> <- + File.write_bytes(f, bytes(10n, 1)) + wrote(p) + +law slot_at: + for r: Array & U32 + for want: U32 + for name: String + IO(Array) + +def slot_at(r, want, name): + (a, got) = r + do IO>: + check(name, U32.is_eq(got, want)) + return a + +law slot: + for a: Array + for +i: U32 + for want: U32 + for name: String + IO(Array) + +def slot(a, i, want, name): + slot_at(Array.get(U32, a, i), want, name) + +law count: + for r: Array & Result<&1, &1, U32 & String, U32> + for want: U32 + for name: String + IO(Array) + +def count(r, want, name): + (a, result) = r + do IO>: + n : U32 <- IO.pass(U32, result) + check(name, U32.is_eq(n, want)) + return a + +law failed: + for r: Array & Result<&1, &1, U32 & String, U32> + for want: U32 + for name: String + IO(Array) + +def failed(r, want, name): + (a, result) = r + match result: + case Done{value}: IO.die(Array, 1, "unexpected success: " ++ name) + case Fail{error}: + (code, message) = error + do IO>: + check(name, U32.is_eq(code, want)) + return a + +law into: + for pair: File & (Array & Result<&1, &1, U32 & String, U32>) + for want: U32 + for name: String + IO(File & Array) + +def into(pair, want, name): + (file, r) = pair + do IO>: + a : Array <- count(r, want, name) + return (file, a) + +law bad: + for pair: File & (Array & Result<&1, &1, U32 & String, U32>) + IO(Array) + +def bad(pair): + (file, r) = pair + do IO>: + a : Array <- failed(r, 9, "read on write-only handle") + File.close(file) + return a + +law last: + for fa: File & Array + IO(Unit) + +def last(fa): + (f, a) = fa + do IO: + a : Array <- slot(a, 0, 67305985, "empty reads leave the array") + File.close(f) + +law eof: + for fa: File & Array + IO(Unit) + +def eof(fa): + (f, a) = fa + do IO: + p : File & (Array & Result<&1, &1, U32 & String, U32>) <- + File.read_into(f, 10, 4, a, 0) + fa : File & Array <- into(p, 0, "read at the file's end") + last(fa) + +law ends: + for fa: File & Array + IO(Unit) + +def ends(fa): + (f, a) = fa + do IO: + a : Array <- slot(a, 3, 100992003, "offset read lands at its slot") + p : File & (Array & Result<&1, &1, U32 & String, U32>) <- + File.read_into(f, 0, 4, a, 4) + fa : File & Array <- into(p, 0, "read at the array's end") + eof(fa) + +law tail: + for fa: File & Array + IO(Unit) + +def tail(fa): + (f, a) = fa + do IO: + a : Array <- slot(a, 0, 67305985, "bytes 1..4 little-endian") + a : Array <- slot(a, 1, 134678021, "bytes 5..8 little-endian") + a : Array <- slot(a, 2, 4294904329, "short tail keeps high bytes") + a : Array <- slot(a, 3, 4294967295, "slot past the bytes untouched") + p : File & (Array & Result<&1, &1, U32 & String, U32>) <- + File.read_into(f, 2, 100, a, 3) + fa : File & Array <- into(p, 4, "read stops at the array's end") + ends(fa) + +law after: + for f: File + for pair: File & (Array & Result<&1, &1, U32 & String, U32>) + IO(Unit) + +def after(f, pair): + do IO: + q : File & (Array & Result<&1, &1, U32 & String, U32>) <- + File.read_into(f, 0, 100, Array.new(U32, 2n, 4294967295), 0) + a : Array <- bad(pair) + a : Array <- slot(a, 0, 7, "failed read leaves the array") + fa : File & Array <- into(q, 10, "read stops at the file's end") + tail(fa) + +law main: + IO(Unit) + +def main(): + do IO: + write() + f : File <- IO.try(File, File.open("/tmp/bend_io_file_read_into", "r")) + w : File <- IO.try(File, File.open("/tmp/bend_io_file_read_into", "a")) + p : File & (Array & Result<&1, &1, U32 & String, U32>) <- + File.read_into(w, 0, 4, Array.new(U32, 2n, 7), 0) + after(f, p) + +#|read on write-only handle +#|failed read leaves the array +#|read stops at the file's end +#|bytes 1..4 little-endian +#|bytes 5..8 little-endian +#|short tail keeps high bytes +#|slot past the bytes untouched +#|read stops at the array's end +#|offset read lands at its slot +#|read at the array's end +#|read at the file's end +#|empty reads leave the array