gzguts.h.lean

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

1import ZlibF.Runtime.Tables
2import ZlibF.Zlib.gzfs
3
4/-!
5# gzguts.h — the header content of the gz* files
6
7Default x86_64 Linux build (`STDC`, `STDC99`, `HAVE_VSNPRINTF`, `_LARGEFILE64_SOURCE` defined; `NO_GZCOMPRESS`,
8`WIDECHAR`, `UNDER_CE`, `NO_snprintf`, `NO_vsnprintf` undefined). The constants `GZBUFSIZE`, `GZ_NONE`, `GZ_READ`,
9`GZ_WRITE`, `GZ_APPEND`, `LOOK`, `GZIP`, the struct `gz_state` and `gzFile_s` come from the generated schema.
10`COPY` of `gzguts.h` is `GZ_COPY` in the runtime (the name `COPY` is the inflate enumerator).
11
12Decisions (see `docs/design/external-io.md`):
13
14* `gzFile` is `GzFilePtr` (`some (.in_gzstate_x id)`), `gz_statep` is `GzStatePtr` (`some (.tab id)`); the cast
15  `(gz_statep)file` is `castState`, `(gzFile)state` is `castFile`.
16* `&(state->strm)` is `strmOf state`, computed without a dereference.
17* Locals whose address is taken (`unsigned char buf[1]`) are blocks made by `allocLocal` (no allocation oracle:
18  automatic storage cannot fail) and freed before every return.
19* A pointer to a scalar (`int *errnum`, `z_size_t *destLen`) is a pointer to a byte block holding the value in
20  little-endian order (`load32`, `store32`, `load64`, `store64`), because the runtime has no pointer to a single cell.
21* Signed arithmetic is checked (`i64add`, `i64sub`, `i64neg`: overflow is `Fault.ub`).
22-/
23
24namespace Zlib.Gzguts
25open C Zlib.GzFs
26
27/-- `(gz_statep)file` -/
28def castState (f : GzFilePtr) : GzStatePtr :=
29  f.map fun | .in_gzstate_x i => .tab i
30
31/-- `(gzFile)state` -/
32def castFile (s : GzStatePtr) : GzFilePtr :=
33  s.map fun | .tab i => .in_gzstate_x i
34
35/-- `&(state->strm)` -/
36def strmOf (s : GzStatePtr) : ZStreamPtr :=
37  s.map fun | .tab i => .in_gzstate_strm i
38
39/-- `*state` -/
40def ldS (s : GzStatePtr) : M GzState := ldGzState s
41
42/-- `*state = f(*state)`: a field write. -/
43def updS (s : GzStatePtr) (f : GzState → GzState) : M Unit := do
44  stGzState s (f (← ldGzState s))
45
46/-- A field write of `state->x`. -/
47def updX (s : GzStatePtr) (f : GzFile → GzFile) : M Unit :=
48  updS s fun st => { st with x := f st.x }
49
50/-- `*strm` -/
51def ldZ (z : ZStreamPtr) : M ZStream := ldZStream z
52
53/-- A field write of `*strm`. -/
54def updZ (z : ZStreamPtr) (f : ZStream → ZStream) : M Unit := do
55  stZStream z (f (← ldZStream z))
56
57/-- Checked `z_off64_t` arithmetic: signed overflow is undefined. -/
58def i64chk (r : Int) : M Int64 :=
59  if -9223372036854775808 ≤ r ∧ r < 9223372036854775808 then pure (Int64.ofInt r) else C.ub "signed overflow (long)"
60def i64add (a b : Int64) : M Int64 := i64chk (a.toInt + b.toInt)
61def i64sub (a b : Int64) : M Int64 := i64chk (a.toInt - b.toInt)
62def i64neg (a : Int64) : M Int64 := i64chk (-a.toInt)
63
64/-- `(z_off64_t)u` for an unsigned 32-bit value. -/
65def u32ToI64 (u : UInt32) : Int64 := Int64.ofNat u.toNat
66
67/-- `GZ_OFF_MAX`: `((((z_off64_t)1 << (sizeof(z_off64_t) * CHAR_BIT - 2)) - 1) * 2 + 1)` -/
68def GZ_OFF_MAX : Int64 := Int64.ofInt 9223372036854775807
69
70/-- A local array: a fresh writable block with arbitrary content, outside the allocation oracle (automatic storage
71cannot fail). Made by the runtime allocator `allocBytes`. -/
72def allocLocal (n : Nat) : M BPtr := fun h =>
73  allocBytes (Array.ofFn (n := n) fun i => Junk.of (h.garbage h.nalloc i.val)) h
74
75/-- `*(int *)p` (the runtime has no pointer to a single `int`: see the file comment). -/
76def load32 (p : BPtr) : M Int32 := do
77  let b0 ← index8 p 0; let b1 ← index8 p 1; let b2 ← index8 p 2; let b3 ← index8 p 3
78  return (b0.toUInt32 ||| (b1.toUInt32 <<< 8) ||| (b2.toUInt32 <<< 16) ||| (b3.toUInt32 <<< 24)).toInt32
79
80/-- `*(int *)p = v` -/
81def store32 (p : BPtr) (v : Int32) : M Unit := do
82  let u := v.toUInt32
83  store8 (← p.add 0) u.toUInt8
84  store8 (← p.add 1) (u >>> 8).toUInt8
85  store8 (← p.add 2) (u >>> 16).toUInt8
86  store8 (← p.add 3) (u >>> 24).toUInt8
87
88/-- `*(uint64_t *)p` -/
89def load64 (p : BPtr) : M UInt64 := do
90  let mut v : UInt64 := 0
91  for i in [0:8] do
92    v := v ||| ((← index8 p i).toUInt64 <<< (8 * i).toUInt64)
93  return v
94
95/-- `*(uint64_t *)p = v` -/
96def store64 (p : BPtr) (v : UInt64) : M Unit := do
97  for i in [0:8] do
98    store8 (← p.add i) (v >>> (8 * i).toUInt64).toUInt8
99
100/-- `memchr(p, c, n)`: reads at most `n` bytes and stops at the first match; faults if a byte it reads is outside
101the object. Returns NULL if there is no match. -/
102def memchrB (p : BPtr) (c : UInt8) (n : Nat) : M BPtr := do
103  for i in [0:n] do
104    if (← index8 p i) == c then return (← p.add i)
105  return .null
106
107end Zlib.Gzguts