File.read_into reads a file's bytes straight into an Array<U32>

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<U32>, at: U32) ->
+  IO(File & (Array<U32> & 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"

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<U32> 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

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);

tests/io/file_read_into.bend

@@ -0,0 +1,209 @@
+# File.read_into lands bytes little-endian in an Array<U32>'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<Unit>:
+    IO.pass(Unit, result)
+    File.close(file)
+
+law write:
+  IO(Unit)
+
+def write():
+  do IO<Unit>:
+    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> & U32
+  for want: U32
+  for name: String
+  IO(Array<U32>)
+
+def slot_at(r, want, name):
+  (a, got) = r
+  do IO<Array<U32>>:
+    check(name, U32.is_eq(got, want))
+    return a
+
+law slot:
+  for a: Array<U32>
+  for +i: U32
+  for want: U32
+  for name: String
+  IO(Array<U32>)
+
+def slot(a, i, want, name):
+  slot_at(Array.get(U32, a, i), want, name)
+
+law count:
+  for r: Array<U32> & Result<&1, &1, U32 & String, U32>
+  for want: U32
+  for name: String
+  IO(Array<U32>)
+
+def count(r, want, name):
+  (a, result) = r
+  do IO<Array<U32>>:
+    n : U32 <- IO.pass(U32, result)
+    check(name, U32.is_eq(n, want))
+    return a
+
+law failed:
+  for r: Array<U32> & Result<&1, &1, U32 & String, U32>
+  for want: U32
+  for name: String
+  IO(Array<U32>)
+
+def failed(r, want, name):
+  (a, result) = r
+  match result:
+    case Done{value}: IO.die(Array<U32>, 1, "unexpected success: " ++ name)
+    case Fail{error}:
+      (code, message) = error
+      do IO<Array<U32>>:
+        check(name, U32.is_eq(code, want))
+        return a
+
+law into:
+  for pair: File & (Array<U32> & Result<&1, &1, U32 & String, U32>)
+  for want: U32
+  for name: String
+  IO(File & Array<U32>)
+
+def into(pair, want, name):
+  (file, r) = pair
+  do IO<File & Array<U32>>:
+    a : Array<U32> <- count(r, want, name)
+    return (file, a)
+
+law bad:
+  for pair: File & (Array<U32> & Result<&1, &1, U32 & String, U32>)
+  IO(Array<U32>)
+
+def bad(pair):
+  (file, r) = pair
+  do IO<Array<U32>>:
+    a : Array<U32> <- failed(r, 9, "read on write-only handle")
+    File.close(file)
+    return a
+
+law last:
+  for fa: File & Array<U32>
+  IO(Unit)
+
+def last(fa):
+  (f, a) = fa
+  do IO<Unit>:
+    a : Array<U32> <- slot(a, 0, 67305985, "empty reads leave the array")
+    File.close(f)
+
+law eof:
+  for fa: File & Array<U32>
+  IO(Unit)
+
+def eof(fa):
+  (f, a) = fa
+  do IO<Unit>:
+    p : File & (Array<U32> & Result<&1, &1, U32 & String, U32>) <-
+      File.read_into(f, 10, 4, a, 0)
+    fa : File & Array<U32> <- into(p, 0, "read at the file's end")
+    last(fa)
+
+law ends:
+  for fa: File & Array<U32>
+  IO(Unit)
+
+def ends(fa):
+  (f, a) = fa
+  do IO<Unit>:
+    a : Array<U32> <- slot(a, 3, 100992003, "offset read lands at its slot")
+    p : File & (Array<U32> & Result<&1, &1, U32 & String, U32>) <-
+      File.read_into(f, 0, 4, a, 4)
+    fa : File & Array<U32> <- into(p, 0, "read at the array's end")
+    eof(fa)
+
+law tail:
+  for fa: File & Array<U32>
+  IO(Unit)
+
+def tail(fa):
+  (f, a) = fa
+  do IO<Unit>:
+    a : Array<U32> <- slot(a, 0, 67305985, "bytes 1..4 little-endian")
+    a : Array<U32> <- slot(a, 1, 134678021, "bytes 5..8 little-endian")
+    a : Array<U32> <- slot(a, 2, 4294904329, "short tail keeps high bytes")
+    a : Array<U32> <- slot(a, 3, 4294967295, "slot past the bytes untouched")
+    p : File & (Array<U32> & Result<&1, &1, U32 & String, U32>) <-
+      File.read_into(f, 2, 100, a, 3)
+    fa : File & Array<U32> <- into(p, 4, "read stops at the array's end")
+    ends(fa)
+
+law after:
+  for f: File
+  for pair: File & (Array<U32> & Result<&1, &1, U32 & String, U32>)
+  IO(Unit)
+
+def after(f, pair):
+  do IO<Unit>:
+    q : File & (Array<U32> & Result<&1, &1, U32 & String, U32>) <-
+      File.read_into(f, 0, 100, Array.new(U32, 2n, 4294967295), 0)
+    a : Array<U32> <- bad(pair)
+    a : Array<U32> <- slot(a, 0, 7, "failed read leaves the array")
+    fa : File & Array<U32> <- into(q, 10, "read stops at the file's end")
+    tail(fa)
+
+law main:
+  IO(Unit)
+
+def main():
+  do IO<Unit>:
+    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<U32> & 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