28 Input, output and files

What to know first

chapter 16, Capabilities · cap io, cap file_system and effects io

chapter 19, Ownership · values needing completion are finished explicitly

chapter 17, Designing failure · at the boundary, report with result

Looking back

In chapter 19, what decided that a type “needs completion”?

A. The existence of an op that takes the type as owned and returns a result. Letting such a value go out of scope without finishing it was rejected with E-OWN-INCOMPLETE. This chapter shows where that rule is most useful — files that must be closed once opened.

The need for this chapter, and its context

Part VIII is about the places a program meets the outside world, and the first is input/output. It is where failure is common — files are missing, disks fill up, reads get cut off. And the most common defects are mixing failure with the end and forgetting to close. Lowent uses capabilities to decide who may do input/output, ownership to make closing unforgettable, and the shape of answers to separate end from failure. Tools built up over the previous four parts come together here.

By the end of this chapter

You will learn to write to standard output with write_out, and to open, close, read and write files with the standard library’s files. You will confirm that a file handle is an owned value needing completion, so forgetting to close it is refused at translation. You will also see why a read’s answer splits three ways, “read · end · failure”, and how to trigger failures on purpose to test them.

The questions this chapter answers

How do you read a file larger than the buffer?

28.1 Standard output#

The only channel to standard output is write_out <cap io> <fd> <bytes>. File descriptor 1 is standard output and 2 is standard error. It returns the number of bytes written. It has already appeared in several chapters, so there is nothing new, but one point is worth making. That this op takes the capability as its first operand means cap io shows in the head of every op that emits even one byte to standard output. There is no debug print slipped in secretly.

28.2 Reading a whole file#

examples/ch28/lines.low

module lines .
rem run: main

use files .

fn is_newline input c u8 . output bool .
do
  return eq c 10 .
end

proc main input out cap io . input fs cap file_system . input al cap allocator .
  output u8 .
  effects io alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 4096 .
  guard is_some g . else return 1 .
  let buf mut slice u8 be some_value g .
  let r result u64 files.file_error be files.slurp fs "notes.txt" buf .
  guard not (is_error r) . else do
    let e u64 be write_out out 1 "cannot read notes.txt\n" .
    return 2 .
  end
  let body slice u8 be subslice buf 0 (ok_value r) .
  let n u64 be pipe body do
    filter is_newline .
    count .
  end .
  let w u64 be write_out out 1 body .
  return narrow u8 n .
end

Output

$ lowentc --run main lines.low
first line
second line
third line
main() = 3

main receives three capabilities: output (cap io), files (cap file_system) and allocation for the buffer (cap allocator). From the head alone you know this program does not touch the network.
files.slurp fs "notes.txt" buf reads the whole file into buf and gives the number of bytes read as a result u64 files.file_error. If the file is missing or larger than the buffer, it is an error. It does not truncate.
On error it writes a message and returns exit code 2 — the shape of handling failure at the boundary (chapter 17).
It cuts off the part read with subslice, counts line breaks with pipe (chapter 24), and writes the contents to standard output as is.

The example reads notes.txt from its own folder. It has three lines, so the exit code is 3.

Q. How do you read a file larger than the buffer?

A. Open it with files.open and repeat files.read. read reads only as much as the buffer, so a file of any size can be read in pieces. A short read is not a failure; giving less than asked is normal, and the caller must keep reading. slurp does exactly that inside.

Reading the 34-byte notes.txt both ways gives this (measured on this edition with different buffer sizes).

 files.slurp  buf 64  ──▶  ok 34
 files.slurp  buf 34  ──▶  ok 34
 files.slurp  buf 33  ──▶  error buffer_too_small
 files.read   buf 16  ──▶  ok (some 16) · ok (some 16) · ok (some 2) · ok none

slurp answers buffer_too_small when the buffer is even one byte smaller than the file; an exact fit is fine. read hands out pieces whatever the buffer size, and joining them is the caller’s job.

28.3 What is opened is closed#

examples/ch28/copy.low

module copy .
rem run: main

use files .

proc main input out cap io . input fs cap file_system . output u8 . effects io .
do
  let o result files.handle files.file_error be files.open fs "../../build/ch28-copy.txt" 1 .
  guard is_ok o . else return 1 .
  var h owned files.handle be ok_value o .
  let w result u64 files.file_error be files.write fs h "hello, file\n" .
  let c result void files.file_error be files.close fs h .
  guard is_ok w . else return 2 .
  guard is_ok c . else return 3 .
  let m u64 be write_out out 1 "wrote and closed\n" .
  return 0 .
end

Output

$ lowentc --run main copy.low
wrote and closed
main() = 0

files.open fs <path> 1 opens for writing. Modes are 0 read, 1 write (truncate and create), 2 append.
On success, ok_value o is put into an owned files.handle.
It writes with files.write and closes with files.close fs h. close takes an owned handle and returns a result. Closing really can fail — on network file systems or full disks, failing to flush the last buffer shows up at close.

Because close has that shape, handle is a type needing completion. Leaving it unclosed is rejected.

examples/ch28/forgot.low

module forgot .
rem expect: E-OWN-INCOMPLETE

use files .

proc leak input fs cap file_system . output u8 . effects io .
do
  let o result files.handle files.file_error be files.open fs "notes.txt" 0 .
  guard is_ok o . else return 1 .
  var h owned files.handle be ok_value o .
  return 0 .
end

Output

$ lowentc --check forgot.low
10:0 E-OWN-INCOMPLETE: this value is dropped automatically at the end of scope — but the program itself declares an op that takes this type `owned` BY VALUE and returns a `result`: finishing it CAN FAIL. An automatic drop is a RELEASE (total, non-suspending), and it has nowhere to hand you that failure — it would SWALLOW it. A fallible finish (flush/commit/close) is a COMPLETION and must be EXPLICIT: call it and handle the `result`. If you really mean to discard the value and its failure, say so with `drop`. RFC-0058

A program that forgets to close does not translate. It does not count on the operating system closing file descriptors when the process ends. If you really mean to discard without closing, write drop h . to say so.

The life of one handle, on one page:

 files.open ──▶ ok_value o ──▶ var h owned files.handle
                                    │
     files.write fs h "…"  ◀────────┤  passing h keeps ownership in h
                                    │
     files.close fs h      ◀────────┘  ownership moves into close
            │
            ▼
     result void file_error            closing can fail too

 E-OWN-INCOMPLETE   h left the scope without close
 E-OWN-MOVED        h was used again after close
 drop h .           discard it on purpose, unclosed

Translation rejects the first two. The third is how the intent to discard is left in the source.

A common misconception. Carrying a file handle as a plain integer is lighter

Holding the integer the kernel gave has the same run-time cost; files.handle is a struct holding one integer. The difference is what translation can know. An integer can be copied, forgotten or closed twice without anyone noticing. An owned value moves, is rejected when forgotten, and is rejected when closed twice. Rules are put onto the same bytes.

28.4 End and failure are different answers#

files.read answers in three positions.

Answer	Meaning
`ok (some n)`	`n` bytes were read
`ok none`	The end of the file. Not a failure
`error e`	A failure. `e` says which operation failed

Table 28.1 — The answers of read

Reading a 34-byte file again and again with a 16-byte buffer gives these answers (measured on this edition).

 notes.txt  34 bytes            buf  16 bytes

 read 1   ok (some 16)    bytes  0 .. 15
 read 2   ok (some 16)    bytes 16 .. 31
 read 3   ok (some 2)     bytes 32 .. 33
 read 4   ok none         the end — stop here
 read 5   ok none         reading past the end is still the end

A last piece (2 bytes) smaller than the buffer does not announce the end. The end is announced separately, by ok none.

At one time this module’s slurp just stopped its loop when a read failed. A failed read was then reported as “read the whole file”, and a line-counting program built on the module reported a read failure as the success “0 lines”. The lesson was that one value must not carry two meanings (end and failure), and so the answer became three positions.

Nor were three positions mechanically put on every op. Opening has no “end”, so open is two positions, result handle file_error. The reader in the io module, which reads slices in memory, has nowhere to fail, so it uses only option. The honest shape differs per op.

28.5 Triggering failure on purpose#

File failures rarely happen normally, so code that handles them tends to stay untested. The standard library’s host operations have a fault injector, switched on with an environment variable.

LOW_HOST_FAULT="open:err"        every open fails
LOW_HOST_FAULT="read:err@2"      the second read fails
LOW_HOST_FAULT="read:short@1=4"  the first read is cut to 4 bytes
LOW_HOST_FAULT="close:err"       closing fails

The VM and native code use the same injector, so the two back ends must agree. Running LOW_HOST_FAULT="open:err" lowentc --run main lines.low sends lines.low down its error branch, writes the message and returns 2. It is off by default.

The 16-byte reads from the previous section, run again under the injector, change like this (measured on this edition).

 (no fault)          ok 16 · ok 16 · ok 2  · ok none
 read:short@1=4      ok 4  · ok 16 · ok 14 · ok none
 read:err@2          ok 16 · error read_failed

A short read still adds up to 34, and the end is still announced by ok none. eof_fixed.low returns 34 on both the first and the second row. On the third row the failure arrives as an answer different from the end, so only code that tells the two apart takes this path correctly.

In practice. A defect found by a line-counting program

The injector made the “0 lines” defect above visible. Failing the first read with LOW_HOST_FAULT="read:err@1" made the line count finish successfully. Had the failure path never run, this defect would have stayed hidden until a real disk error. If capabilities and ownership stop “forgetting to close” at translation, the injector reveals “handling failure wrongly” at run time.

28.6 Common mistakes#

Counter-example. Opening in read mode and writing — without checking the byte count

examples/ch28/mistake_readmode.low

module mistake_readmode .
rem run: main

use files .

proc main input out cap io . input fs cap file_system . output u8 . effects io .
do
  rem ✘ mode 0 is read --- yet it writes
  let o result files.handle files.file_error be files.open fs "notes.txt" 0 .
  guard is_ok o . else return 1 .
  var h owned files.handle be ok_value o .
  let w result u64 files.file_error be files.write fs h "extra line\n" .
  let c result void files.file_error be files.close fs h .
  drop c .
  guard is_ok w . else return 2 .
  rem the write failed, so it leaves with 2 here --- a short write is checked too
  guard eq (ok_value w) 11 . else return 3 .
  return 0 .
end

Output

$ lowentc --run main mistake_readmode.low
main() = 2

files.open fs "notes.txt" 0 is read mode. Writing there makes files.write return a failure — a short write with the stream’s error flag set is a failure, not a value — and this example leaves with exit code 2. The same spot used to answer ok 0 (“0 bytes written”), so code that asked only is_ok w passed it as a success. Check the mode (0 read · 1 write · 2 append), and look at the number of bytes written as well as success. A short write means the remaining bytes must be written again.

Counter-example. Writing with a handle that was already closed

examples/ch28/mistake_afterclose.low

module mistake_afterclose .
rem expect: E-OWN-MOVED

use files .

proc main input out cap io . input fs cap file_system . output u8 . effects io .
do
  let o result files.handle files.file_error be files.open fs "../../build/ch28-after.txt" 1 .
  guard is_ok o . else return 1 .
  var h owned files.handle be ok_value o .
  let c result void files.file_error be files.close fs h .
  drop c .
  rem ✘ writes again with the closed handle --- `close` took ownership
  let w result u64 files.file_error be files.write fs h "late\n" .
  drop w .
  return 0 .
end

Output

$ lowentc --check mistake_afterclose.low
mistake_afterclose.low:14:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today

files.close takes an owned handle, so ownership passes the moment it is called. Afterwards h is a handle that no longer exists, so this is E-OWN-MOVED. In C, fwrite after fclose is undefined behaviour, and if the same number was reused by a newly opened file, the bytes land in the wrong file. Ownership stops that at translation time.

Counter-example. Asking only about failure in the answer of a read

examples/ch28/mistake_eof.low

module mistake_eof .
rem trap: main

use files .

proc main input out cap io . input fs cap file_system . input al cap allocator .
  output u8 .
  effects io alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 64 .
  guard is_some g . else return 1 .
  let buf mut slice u8 be some_value g .
  let o result files.handle files.file_error be files.open fs "notes.txt" 0 .
  guard is_ok o . else return 2 .
  var h owned files.handle be ok_value o .
  var total u64 be 0 .
  var i u64 be 0 .
  while lt i 3 . do
    let r result (option u64) files.file_error be files.read fs h buf .
    guard is_ok r . else return 3 .
    rem ✘ only failure is checked --- `some_value` stops at the end-of-file `ok none`
    set total (add total (some_value (ok_value r))) .
    set i (add i 1) .
  end
  let c result void files.file_error be files.close fs h .
  drop c .
  return narrow u8 total .
end

Output

$ lowentc --run main mistake_eof.low
== ir diagnostics (1) ==
0:0 E-VM-NONE: some_value of none (panic)

The answer of files.read has three places. is_ok r only says “not a failure”. The end-of-file ok none is not a failure either, so it passes, and taking some_value out of it stops the program. Split all three places.

examples/ch28/eof_fixed.low

module eof_fixed .
rem run: main

use files .

proc main input out cap io . input fs cap file_system . input al cap allocator .
  output u8 .
  effects io alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 16 .
  guard is_some g . else return 1 .
  let buf mut slice u8 be some_value g .
  let o result files.handle files.file_error be files.open fs "notes.txt" 0 .
  guard is_ok o . else return 2 .
  var h owned files.handle be ok_value o .
  var total u64 be 0 .
  var more bool be true .
  var rounds u64 be 0 .
  while and more (lt rounds 100) . do
    let r result (option u64) files.file_error be files.read fs h buf .
    guard is_ok r . else do
      let c1 result void files.file_error be files.close fs h .
      drop c1 .
      return 3 .
    end
    rem split all three places --- read · end · failure
    let got option u64 be ok_value r .
    if is_some got . do
      set total (add total (some_value got)) .
    end else do
      set more false .
    end
    set rounds (add rounds 1) .
  end
  let c result void files.file_error be files.close fs h .
  guard is_ok c . else return 4 .
  return narrow u8 total .
end

Output

$ lowentc --run main eof_fixed.low
main() = 34

It reads the 34-byte file in three pieces with a 16-byte buffer and stops at the ok none of the fourth read. On failure it closes and returns 3; if closing fails, it returns 4. The bound on rounds makes the loop end even for a source that never reports its end.

A common misconception. slurp of a file larger than the buffer reads just the beginning

examples/ch28/slurp_small.low

module slurp_small .
rem run: main

use files .

proc main input out cap io . input fs cap file_system . input al cap allocator .
  output u8 .
  effects io alloc .
do
  rem an 8-byte buffer for a 34-byte file
  let g option mut slice u8 be alloc_bytes al capacity 8 .
  guard is_some g . else return 1 .
  let buf mut slice u8 be some_value g .
  let r result u64 files.file_error be files.slurp fs "notes.txt" buf .
  rem it does not come back cut to the first 8 bytes --- it is an error
  guard not (is_error r) . else return 2 .
  return narrow u8 (ok_value r) .
end

Output

$ lowentc --run main slurp_small.low
main() = 2

slurp of a 34-byte file into an 8-byte buffer returns an error, not the first 8 bytes. This prevents the bug of trusting truncated content as the whole file — the tail of a configuration file silently disappearing. If a file may be larger than the buffer, read it in pieces with files.open and files.read.

28.7 This chapter’s syntax at a glance#

Shape	Meaning	Why
`write_out out 1 "…"`	write to standard output (1) · standard error (2) — returns the count	the capability comes first — no hidden printing
`use files .` + `input fs cap file_system .`	the file module and its capability	the head shows whether files are reached
`files.open fs "notes.txt" 0`	open — 0 read · 1 write · 2 append · `result handle file_error`	opening has no “end” — two places
`var h owned files.handle be ok_value o .`	hold the handle as owned	forgetting it: `E-OWN-INCOMPLETE` · writing after close: `E-OWN-MOVED`
`files.read fs h buf`	`ok (some n)` read · `ok none` end · `error e` failure	one value never carries two meanings
`files.write fs h bytes`	returns the count as a `result`	writes can be short — check the count
`files.close fs h`	takes `owned`, returns `result` — completion	closing can fail too
`files.slurp fs path buf`	read it whole — an error if larger than the buffer	never truncates
`LOW_HOST_FAULT="read:err@2"`	inject failures on purpose (environment variable)	exercise the failure paths

Table 28.2 — I/O and file syntax — shape · meaning · why it looks this way

Recap

Standard output is write_out <cap io> <fd> <bytes>, with the capability as first operand. The files module takes cap file_system to open, close, read and write files. A file handle needs completion because close takes it owned and returns a result, so forgetting to close is refused at translation. read answers in three positions — read, end, failure — and failure paths are exercised on purpose with the LOW_HOST_FAULT injector.

← PrevContentsNext →