gzfs.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Runtime.Alloc
2
3/-!
4# gzfs: the external world of the gz* files (trusted base)
5
6The runtime heap (`ZlibF/Runtime`) has no file system, no `errno` and no `printf`. The gz* functions call `open`,
7`read`, `write`, `lseek`, `close`, `fcntl`, `strerror`, `snprintf`/`vsnprintf`. This file is the model of those
8calls, written next to the translation; it is part of the trusted base (`docs/design/external-io.md`
9lists every decision and narrowing).
10
11The world is a record `Fs` that lives beside the heap: a gz computation is `G α = StateT Fs C.M α`, so a heap
12computation (`C.M`) lifts into it and a fault is still `Fault.ub`.
13-/
14
15namespace Zlib.GzFs
16open C
17
18/-- An open file description (what a file descriptor refers to). -/
19structure OFile where
20  node : Nat
21  pos : Nat
22  rd : Bool
23  wr : Bool
24  append : Bool
25  deriving Inhabited
26
27/-- A file (its bytes) or a directory (no bytes; `open` for reading succeeds, `read` fails with `EISDIR`). -/
28structure Node where
29  data : Array UInt8
30  isDir : Bool
31  deriving Inhabited
32
33/-- The file system, the descriptor table, `errno` and the file size limit (`RLIMIT_FSIZE`). Paths are flat
34byte strings (no directory structure). -/
35structure Fs where
36  names : Array (Array UInt8 × Nat) := #[]
37  nodes : Array Node := #[]
38  fds : Array (Option OFile) := #[]
39  errno : Int32 := 0
40  fsizeLimit : Nat := 2 ^ 62
41  deriving Inhabited
42
43/-- A gz computation: the world in, the heap in, a value and both out, or a fault. -/
44abbrev G (α : Type) : Type := StateT Fs M α
45
46/-- Undefined behaviour inside `G`. -/
47def gub {α : Type} (what : String) : G α := fun _ => C.ub what
48
49/-- `ENOENT` etc. (Linux x86_64 values). -/
50def ENOENT : Int32 := 2
51def EBADF : Int32 := 9
52def EEXIST : Int32 := 17
53def EISDIR : Int32 := 21
54def EINVAL : Int32 := 22
55def EFBIG : Int32 := 27
56def ENOSPC : Int32 := 28
57def EOVERFLOW : Int32 := 75
58def EAGAIN : Int32 := 11
59
60/-- `errno` as read by the C. -/
61def getErrno : G Int32 := do return (← get).errno
62/-- `errno = e`. -/
63def setErrno (e : Int32) : G Unit := modify fun w => { w with errno := e }
64
65/-- `BLOCKED(e)`: `e == EAGAIN || e == EWOULDBLOCK` (both are 11). -/
66def BLOCKED (e : Int32) : Bool := e == EAGAIN
67
68/-- The text of `strerror(e)` (glibc), for the errno values the model can produce; others give glibc's
69`Unknown error N`. -/
70def strerrorText (e : Int32) : String :=
71  if e == 0 then "Success"
72  else if e == ENOENT then "No such file or directory"
73  else if e == EBADF then "Bad file descriptor"
74  else if e == EEXIST then "File exists"
75  else if e == EISDIR then "Is a directory"
76  else if e == EINVAL then "Invalid argument"
77  else if e == EFBIG then "File too large"
78  else if e == ENOSPC then "No space left on device"
79  else if e == EOVERFLOW then "Value too large for defined data type"
80  else s!"Unknown error {e.toInt}"
81
82/-- A string literal of the C sources: the static read-only array of the runtime (`strLitRef`, the same pointer
83every time). -/
84def strLit (s : String) : M BPtr := strLitRef s
85
86/-- The text returned by `strerror(e)`: a string of the C library, not of the sources, so it is not in `strTable`.
87Modelled as a fresh read-only block (never freed). -/
88def libcStr (s : String) : M BPtr := allocBytesRO (s.toUTF8.toList.toArray.push 0)
89
90/-- `strerror(errno)`: a pointer to a string. -/
91def zstrerror : G BPtr := do
92  let e ← getErrno
93  libcStr (strerrorText e)
94
95/-- The bytes of the NUL-terminated string at `p` (without the NUL). Faults if `p` is null or has no NUL. -/
96def cstring (p : BPtr) : M (Array UInt8) := do
97  let n ← strlenB p
98  let mut out : Array UInt8 := #[]
99  for i in [0:n.toNat] do
100    out := out.push (← index8 p i)
101  return out
102
103/-- Store `bs` at `p`, `p + 1`, ... as one block copy (what `read` and `vsnprintf` do to their buffer): faults if the
104range is not inside the object or the object is read-only. (One copy instead of a store per byte: every store makes the
105heap function one level deeper, which costs memory in the interpreter, not in the model.) -/
106def storeBytes (p : BPtr) (bs : Array UInt8) : M Unit := do
107  if bs.isEmpty then return
108  let t ← allocBytes bs
109  memcpyB p t bs.size
110  freeB t
111
112/-- Load `n` bytes from `p`. -/
113def loadBytes (p : BPtr) (n : Nat) : M (Array UInt8) := do
114  let mut out : Array UInt8 := #[]
115  for i in [0:n] do
116    out := out.push (← index8 p i)
117  return out
118
119/-! ## System calls -/
120
121def O_WRONLY : Int32 := 1
122def O_CREAT : Int32 := 64
123def O_EXCL : Int32 := 128
124def O_TRUNC : Int32 := 512
125def O_APPEND : Int32 := 1024
126def O_NONBLOCK : Int32 := 2048
127def O_CLOEXEC : Int32 := 524288
128def O_LARGEFILE : Int32 := 0
129def SEEK_SET : Int32 := 0
130def SEEK_CUR : Int32 := 1
131def SEEK_END : Int32 := 2
132
133private def findName (w : Fs) (p : Array UInt8) : Option Nat :=
134  (w.names.find? (fun e => e.1 == p)).map (·.2)
135
136private def lowestFd (w : Fs) : Nat :=
137  let rec go (i : Nat) : Nat → Nat
138    | 0 => i
139    | k + 1 => if i < w.fds.size then (if (w.fds[i]!).isNone then i else go (i + 1) k) else i
140  go 3 (w.fds.size + 3)
141
142/-- `open(path, oflag, 0666)` for `path` given as its bytes. Returns the descriptor or -1 with `errno`. The
143access mode is read-only or write-only; `O_CREAT`, `O_EXCL`, `O_TRUNC`, `O_APPEND` are honoured; `O_NONBLOCK`,
144`O_CLOEXEC` and `O_LARGEFILE` do nothing (regular files only). Permissions are not modelled. -/
145def fsOpen (path : Array UInt8) (oflag : Int32) : G Int32 := fun w =>
146  let acc := oflag &&& 3
147  let has (f : Int32) := (oflag &&& f) != 0
148  let fail (e : Int32) : M (Int32 × Fs) := pure (-1, { w with errno := e })
149  let openNode (n : Nat) (w : Fs) : M (Int32 × Fs) :=
150    let node := w.nodes[n]!
151    let wr := acc == 1
152    if wr && node.isDir then pure (-1, { w with errno := EISDIR })
153    else
154      let w := if wr && has O_TRUNC then { w with nodes := w.nodes.set! n { node with data := #[] } } else w
155      let fd := lowestFd w
156      let fds := if fd < w.fds.size then w.fds else w.fds ++ Array.replicate (fd + 1 - w.fds.size) none
157      let of : OFile := { node := n, pos := 0, rd := acc == 0, wr, append := has O_APPEND }
158      pure (Int32.ofNat fd, { w with fds := fds.set! fd (some of) })
159  if acc ≥ 2 then fail EINVAL
160  else if path.isEmpty then fail ENOENT
161  else match findName w path with
162    | some n => if has O_CREAT && has O_EXCL then fail EEXIST else openNode n w
163    | none =>
164      if has O_CREAT then
165        let n := w.nodes.size
166        openNode n { w with names := w.names.push (path, n), nodes := w.nodes.push { data := #[], isDir := false } }
167      else fail ENOENT
168
169/-- `read(fd, buf, n)` as a pair: the result and the bytes that were read (to be stored at `buf` by the caller). -/
170def fsRead (fd : Int32) (n : UInt64) : G (Int64 × Array UInt8) := fun w =>
171  let fail (e : Int32) : M ((Int64 × Array UInt8) × Fs) := pure ((-1, #[]), { w with errno := e })
172  if fd < 0 || fd.toInt ≥ w.fds.size then fail EBADF
173  else match w.fds[fd.toInt.toNat]! with
174    | none => fail EBADF
175    | some of =>
176      if !of.rd then fail EBADF
177      else
178        let node := w.nodes[of.node]!
179        if node.isDir then fail EISDIR
180        else
181          let k := min n.toNat (node.data.size - of.pos)
182          let bs := node.data.extract of.pos (of.pos + k)
183          pure ((Int64.ofNat k, bs),
184            { w with fds := w.fds.set! fd.toInt.toNat (some { of with pos := of.pos + k }) })
185
186/-- `write(fd, buf, n)` for the bytes `bs` of the buffer. A write past the size limit is cut (a short write), and
187a write with no room fails with `EFBIG`. -/
188def fsWrite (fd : Int32) (bs : Array UInt8) : G Int64 := fun w =>
189  let fail (e : Int32) : M (Int64 × Fs) := pure (-1, { w with errno := e })
190  if fd < 0 || fd.toInt ≥ w.fds.size then fail EBADF
191  else match w.fds[fd.toInt.toNat]! with
192    | none => fail EBADF
193    | some of =>
194      if !of.wr then fail EBADF
195      else if bs.isEmpty then pure (0, w)
196      else
197        let node := w.nodes[of.node]!
198        let pos := if of.append then node.data.size else of.pos
199        if pos ≥ w.fsizeLimit then fail EFBIG
200        else
201          let k := min bs.size (w.fsizeLimit - pos)
202          let old := if pos > node.data.size then node.data ++ Array.replicate (pos - node.data.size) 0 else node.data
203          let new := old.extract 0 pos ++ bs.extract 0 k ++ old.extract (pos + k) old.size
204          pure (Int64.ofNat k,
205            { w with nodes := w.nodes.set! of.node { node with data := new }
206                     fds := w.fds.set! fd.toInt.toNat (some { of with pos := pos + k }) })
207
208/-- `lseek(fd, off, whence)`. -/
209def fsLseek (fd : Int32) (off : Int64) (whence : Int32) : G Int64 := fun w =>
210  let fail (e : Int32) : M (Int64 × Fs) := pure (-1, { w with errno := e })
211  if fd < 0 || fd.toInt ≥ w.fds.size then fail EBADF
212  else match w.fds[fd.toInt.toNat]! with
213    | none => fail EBADF
214    | some of =>
215      let base : Option Int :=
216        if whence == SEEK_SET then some 0
217        else if whence == SEEK_CUR then some of.pos
218        else if whence == SEEK_END then some (w.nodes[of.node]!.data.size) else none
219      match base with
220      | none => fail EINVAL
221      | some b =>
222        let np := b + off.toInt
223        if np < 0 then fail EINVAL
224        else if np > 9223372036854775807 then fail EOVERFLOW
225        else pure (Int64.ofInt np,
226          { w with fds := w.fds.set! fd.toInt.toNat (some { of with pos := np.toNat }) })
227
228/-- `close(fd)`. -/
229def fsClose (fd : Int32) : G Int32 := fun w =>
230  if fd < 0 || fd.toInt ≥ w.fds.size then pure (-1, { w with errno := EBADF })
231  else match w.fds[fd.toInt.toNat]! with
232    | none => pure (-1, { w with errno := EBADF })
233    | some _ => pure (0, { w with fds := w.fds.set! fd.toInt.toNat none })
234
235/-- `fcntl(fd, F_SETFL / F_SETFD, ...)` as used by `gz_open`: the result is ignored by the C and regular files
236do not change behaviour, so it does nothing. -/
237def fsFcntl (_fd : Int32) : G Unit := pure ()
238
239/-! ## Harness access to the world (not C operations) -/
240
241/-- Create or replace the file `name`. -/
242def Fs.put (w : Fs) (name : Array UInt8) (data : Array UInt8) : Fs :=
243  match findName w name with
244  | some n => { w with nodes := w.nodes.set! n { data, isDir := false } }
245  | none => { w with names := w.names.push (name, w.nodes.size), nodes := w.nodes.push { data, isDir := false } }
246
247/-- Create a directory entry `name`. -/
248def Fs.mkdir (w : Fs) (name : Array UInt8) : Fs :=
249  { w with names := w.names.push (name, w.nodes.size), nodes := w.nodes.push { data := #[], isDir := true } }
250
251/-- The bytes of the file `name`, if any. -/
252def Fs.get? (w : Fs) (name : Array UInt8) : Option (Array UInt8) :=
253  (findName w name).map fun n => w.nodes[n]!.data
254
255/-- The position of the descriptor, if open. -/
256def Fs.posOf? (w : Fs) (fd : Nat) : Option Nat :=
257  if h : fd < w.fds.size then (w.fds[fd]).map (·.pos) else none
258
259/-! ## Loops in `G` -/
260
261def gwhile {σ : Type} (cond : σ → G (Bool × σ)) (body : σ → G σ) (s : σ) : G σ :=
262  go C.fuel s
263where
264  go : Nat → σ → G σ
265    | 0, _ => fun _ => fun _ => .error .outOfFuel
266    | n + 1, s => do
267      let (c, s) ← cond s
268      if c then go n (← body s) else pure s
269
270def gdoWhile {σ : Type} (body : σ → G σ) (cond : σ → G (Bool × σ)) (s : σ) : G σ :=
271  go C.fuel s
272where
273  go : Nat → σ → G σ
274    | 0, _ => fun _ => fun _ => .error .outOfFuel
275    | n + 1, s => do
276      let s ← body s
277      let (c, s) ← cond s
278      if c then go n s else pure s
279
280/-! ## printf -/
281
282/-- One variadic argument. `int`/`uint` are 32-bit, `long`/`ulong` 64-bit, `str` is a `char *`. -/
283inductive VaArg where
284  | int (v : Int32)
285  | uint (v : UInt32)
286  | long (v : Int64)
287  | ulong (v : UInt64)
288  | str (p : BPtr)
289
290structure Spec where
291  minus : Bool := false
292  zero : Bool := false
293  plus : Bool := false
294  space : Bool := false
295  alt : Bool := false
296  width : Nat := 0
297  prec : Option Nat := none
298  long : Bool := false
299  conv : UInt8 := 0
300  deriving DecidableEq
301
302def isDigit (c : UInt8) : Bool := 48 ≤ c && c ≤ 57
303
304/-- The decimal number that starts at `j` (at most `fuel` digits) added to `v`: its value and the position after it. -/
305def readNumGo (f : Array UInt8) : Nat → Nat → Nat → Nat × Nat
306  | 0, j, v => (v, j)
307  | k + 1, j, v =>
308    if j < f.size && isDigit f[j]! then readNumGo f k (j + 1) (v * 10 + (f[j]!.toNat - 48)) else (v, j)
309
310/-- The decimal number that starts at `i` and the position after it. -/
311def readNum (f : Array UInt8) (i : Nat) : Nat × Nat := readNumGo f f.size i 0
312
313/-- The flags `-0+ #` that start at `j` (at most `fuel` of them), set in `sp`, and the position after them. -/
314def parseFlags (f : Array UInt8) : Nat → Nat → Spec → Spec × Nat
315  | 0, j, sp => (sp, j)
316  | k + 1, j, sp =>
317    if j < f.size then
318      if f[j]! == 45 then parseFlags f k (j + 1) { sp with minus := true }
319      else if f[j]! == 48 then parseFlags f k (j + 1) { sp with zero := true }
320      else if f[j]! == 43 then parseFlags f k (j + 1) { sp with plus := true }
321      else if f[j]! == 32 then parseFlags f k (j + 1) { sp with space := true }
322      else if f[j]! == 35 then parseFlags f k (j + 1) { sp with alt := true }
323      else (sp, j)
324    else (sp, j)
325
326/-- The conversion specification that starts at `i` (after the `%`): flags, width, precision, length modifier and
327conversion character, and the position after it; `none` if the format ends first. -/
328def parseSpec (f : Array UInt8) (i : Nat) : Option (Spec × Nat) :=
329  let (sp, j) := parseFlags f f.size i {}
330  let (w, j) := readNum f j
331  let sp := { sp with width := w }
332  let (sp, j) :=
333    if j < f.size && f[j]! == 46 then
334      let (p, j3) := readNum f (j + 1)
335      ({ sp with prec := some p }, j3)
336    else (sp, j)
337  let (sp, j) :=
338    if j < f.size && (f[j]! == 108 || f[j]! == 122 || f[j]! == 106 || f[j]! == 116) then
339      ({ sp with long := true }, if j + 1 < f.size && f[j + 1]! == 108 then j + 2 else j + 1)
340    else (sp, j)
341  if j < f.size then some ({ sp with conv := f[j]! }, j + 1) else none
342
343def natDigits (v : Nat) (base : Nat) (upper : Bool) : Array UInt8 :=
344  (Nat.toDigits base v).toArray.map fun c =>
345    let b := c.toNat.toUInt8
346    if upper && b ≥ 97 then b - 32 else b
347
348def pad (sp : Spec) (body : Array UInt8) (zeroOk : Bool) : Array UInt8 :=
349  if body.size ≥ sp.width then body
350  else
351    let n := sp.width - body.size
352    if sp.minus then body ++ Array.replicate n 32
353    else if sp.zero && zeroOk then
354      -- zeros go after the sign / prefix: callers pass sign/prefix separately, see fmtInt
355      Array.replicate n 48 ++ body
356    else Array.replicate n 32 ++ body
357
358def fmtInt (sp : Spec) (neg : Bool) (mag : Nat) (base : Nat) (upper : Bool) (signed : Bool) :
359    Array UInt8 :=
360  let ds0 := natDigits mag base upper
361  let ds1 := match sp.prec with
362    | some 0 => if mag == 0 then #[] else ds0
363    | some p => if ds0.size < p then Array.replicate (p - ds0.size) 48 ++ ds0 else ds0
364    | none => ds0
365  let prefixB : Array UInt8 :=
366    if signed then (if neg then #[45] else if sp.plus then #[43] else if sp.space then #[32] else #[])
367    else if sp.alt && mag != 0 && base == 16 then (if upper then #[48, 88] else #[48, 120])
368    else #[]
369  let ds1 := if sp.alt && base == 8 && (ds1.isEmpty || ds1[0]! != 48) then #[48] ++ ds1 else ds1
370  let total := prefixB.size + ds1.size
371  if total ≥ sp.width then prefixB ++ ds1
372  else
373    let n := sp.width - total
374    if sp.minus then prefixB ++ ds1 ++ Array.replicate n 32
375    else if sp.zero && sp.prec.isNone then prefixB ++ Array.replicate n 48 ++ ds1
376    else Array.replicate n 32 ++ prefixB ++ ds1
377
378/-- The text of a `%s` argument: `(null)` for a null pointer (as glibc), else what the heap resolver `res` gives. -/
379def argStr (res : BPtr → Option (Array UInt8)) (p : BPtr) : Option (Array UInt8) :=
380  if p == .null then some "(null)".toUTF8.toList.toArray else res p
381
382/-- The output of `printf(f, args)` from position `i` on, as bytes, appended to `out`; `res p` is the string at `p` in
383the heap (`none` if there is none). `fuel` is the number of steps left (`f.size + 1` suffices: each step consumes a
384character). Supports `%%`, `%c`, `%s`, `%d`, `%i`, `%u`, `%x`, `%X`, `%o` with the flags `-0+ #`, a width, a
385precision and the length modifiers `l`, `ll`, `z`, `j`, `t`. Anything else, an argument of the wrong kind, or too few
386arguments is an error (undefined in C). -/
387def formatGo (f : Array UInt8) (res : BPtr → Option (Array UInt8)) :
388    Nat → Nat → List VaArg → Array UInt8 → Except String (Array UInt8)
389  | 0, _, _, out => .ok out
390  | fuel + 1, i, args, out =>
391    if i < f.size then
392      if f[i]! != 37 then formatGo f res fuel (i + 1) args (out.push f[i]!)
393      else
394        match parseSpec f (i + 1) with
395        | none => .error "printf: incomplete conversion"
396        | some (sp, j) =>
397          let cv := sp.conv
398          if cv == 37 then formatGo f res fuel j args (out.push 37)
399          else if cv == 99 then
400            match args with
401            | .int v :: r => formatGo f res fuel j r (out ++ pad sp #[v.toUInt32.toUInt8] false)
402            | _ => .error "printf: %c needs an int"
403          else if cv == 115 then
404            match args with
405            | .str p :: r =>
406              match argStr res p with
407              | some s =>
408                let s := match sp.prec with | some k => s.extract 0 k | none => s
409                formatGo f res fuel j r (out ++ pad sp s false)
410              | none => .error "printf: %s argument is not a NUL-terminated string"
411            | _ => .error "printf: %s needs a pointer"
412          else if cv == 100 || cv == 105 then
413            match sp.long, args with
414            | false, .int v :: r =>
415              formatGo f res fuel j r (out ++ fmtInt sp (v.toInt < 0) v.toInt.natAbs 10 false true)
416            | true, .long v :: r =>
417              formatGo f res fuel j r (out ++ fmtInt sp (v.toInt < 0) v.toInt.natAbs 10 false true)
418            | _, _ => .error "printf: %d argument of the wrong kind"
419          else if cv == 117 || cv == 120 || cv == 88 || cv == 111 then
420            let base := if cv == 117 then 10 else if cv == 111 then 8 else 16
421            match sp.long, args with
422            | false, .uint v :: r => formatGo f res fuel j r (out ++ fmtInt sp false v.toNat base (cv == 88) false)
423            | false, .int v :: r =>
424              formatGo f res fuel j r (out ++ fmtInt sp false v.toUInt32.toNat base (cv == 88) false)
425            | true, .ulong v :: r => formatGo f res fuel j r (out ++ fmtInt sp false v.toNat base (cv == 88) false)
426            | true, .long v :: r =>
427              formatGo f res fuel j r (out ++ fmtInt sp false v.toUInt64.toNat base (cv == 88) false)
428            | _, _ => .error "printf: unsigned conversion argument of the wrong kind"
429          else .error "printf: conversion not modelled"
430    else .ok out
431
432/-- The string at `p` in the heap `h` (the bytes before the first NUL), if there is one. -/
433def heapStr (h : Heap) (p : BPtr) : Option (Array UInt8) :=
434  match cstring p h with | .ok (s, _) => some s | .error _ => none
435
436/-- The full output of `printf(fmt, args)` as bytes (`formatGo`); the heap is read, not changed. -/
437def formatBytes (f : Array UInt8) (args : List VaArg) : M (Array UInt8) := fun h =>
438  match formatGo f (heapStr h) (f.size + 1) 0 args #[] with
439  | .ok out => .ok (out, h)
440  | .error m => .error (.ub m)
441
442/-- `vsnprintf(dst, size, fmt, args)`: writes at most `size - 1` characters and a NUL (nothing if `size` is 0) and
443returns the length the full output has. -/
444def vsnprintf (dst : BPtr) (size : UInt64) (fmt : BPtr) (args : List VaArg) : M Int32 := do
445  let f ← cstring fmt
446  let out ← formatBytes f args
447  if out.size > 2147483647 then C.ub "vsnprintf: output longer than INT_MAX"
448  if size != 0 then
449    let k := min out.size (size.toNat - 1)
450    storeBytes dst (out.extract 0 k)
451    let q ← dst.add k
452    store8 q 0
453  return Int32.ofNat out.size
454
455end Zlib.GzFs