gzread.c.lean

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

1import ZlibF.Zlib.«gzlib.c»
2import ZlibF.Zlib.«inflate.c»
3
4/-!
5# gzread.c — faithful translation
6
7Source: `gzread.c` of the verified source (unpatched), default x86_64 Linux build (`errno`, `EAGAIN == EWOULDBLOCK`,
8`STDC`). Reads go through `Zlib.GzFs`.
9
10Patches that the earlier repository applied and that this translation does NOT contain (the faults are kept):
11* **`gz_fetch`, `case COPY`** (R-2, upstream PR 1363): `x.next = out` is set after `gz_load`, so a failing `read`
12  that returned some bytes leaves `x.have != 0` with a stale `x.next`; the readers then copy from it (an overread).
13  The translation follows the C, so the overread is a `Fault.ub` (or a read of the stale buffer).
14* **`gz_read` L406** (R-4, proposed): `x.next` is left pointing into the user's buffer after a direct decompression;
15  a later `gzseek`/`gzdirect` computes `x.next + 0` on it. If the user freed that buffer, `Ptr.add` faults.
16* **`gz_skip_have`** (R-3): `x.next += n` is `NULL + 0` on a fresh state (the model allows it).
17
18Decisions: `unsigned *have` of `gz_load` is returned (the caller stores it right after the call; nothing in `gz_load`
19observes the aliased cell); `unsigned char buf[1]` of `gzgetc` is a local block; `memchr` is `memchrB`.
20-/
21
22namespace Zlib.Gzread
23open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib
24open Zlib.Inflate (inflateInit2_ inflateReset inflate inflateEnd)
25
26structure LoadLoop where
27  «have» : UInt32
28  ret : Int32
29  brk : Bool
30
31/-- `local int gz_load(gz_statep state, unsigned char *buf, unsigned len, unsigned *have)`; `*have` is the second
32component of the result. -/
33def gz_load (state : GzStatePtr) (buf : BPtr) (len : UInt32) : G (Int32 × UInt32) := do
34  -- unsigned get, max = ((unsigned)-1 >> 2) + 1;
35  let max : UInt32 := (((0 : UInt32) - 1) >>> 2) + 1
36  -- state->again = 0; errno = 0; *have = 0;
37  updS state fun s => { s with again := 0 }
38  setErrno 0
39  let l ← gdoWhile
40    (fun (l : LoadLoop) => do
41      -- get = len - *have; if (get > max) get = max;
42      let mut get := len - l.«have»
43      if get > max then get := max
44      -- ret = (int)read(state->fd, buf + *have, get); if (ret <= 0) break;
45      let s ← ldS state
46      let p ← buf.add l.«have».toNat
47      let (r, bs) ← fsRead s.fd get.toUInt64
48      storeBytes p bs
49      let ret := r.toInt32
50      if ret ≤ 0 then return { l with ret, brk := true }
51      -- *have += (unsigned)ret;
52      return { l with ret, «have» := l.«have» + ret.toUInt32 })
53    (fun l => pure (!l.brk && l.«have» < len, l))
54    { «have» := 0, ret := 0, brk := false }
55  -- if (ret < 0) { ... }
56  if l.ret < 0 then
57    let e ← getErrno
58    if BLOCKED e then
59      updS state fun s => { s with again := 1 }
60      if l.«have» != 0 then return (0, l.«have»)
61    gz_error state Z_ERRNO (← zstrerror)
62    return (-1, l.«have»)
63  -- if (ret == 0) state->eof = 1;
64  if l.ret == 0 then updS state fun s => { s with eof := 1 }
65  return (0, l.«have»)
66
67/-- `local int gz_avail(gz_statep state)` -/
68def gz_avail (state : GzStatePtr) : G Int32 := do
69  let strm := strmOf state
70  let s ← ldS state
71  -- if (state->err != Z_OK && state->err != Z_BUF_ERROR) return -1;
72  if s.err != Z_OK && s.err != Z_BUF_ERROR then return -1
73  -- if (state->eof == 0) { ... }
74  if s.eof == 0 then
75    let z ← ldZ strm
76    -- if (strm->avail_in) { copy what's there to the start }
77    if z.avail_in != 0 then
78      let p := s.«in»
79      let q := z.next_in
80      if q != p then
81        -- do { *p++ = *q++; } while (--n);
82        let _ ← cdoWhile
83          (fun (st : BPtr × BPtr × UInt32) => do
84            let (p, q, n) := st
85            let b ← load8 q
86            store8 p b
87            return (← p.add 1, ← q.add 1, n))
88          (fun (st : BPtr × BPtr × UInt32) => do
89            let (p, q, n) := st
90            let n := n - 1
91            pure (n != 0, (p, q, n)))
92          (p, q, z.avail_in)
93    -- if (gz_load(state, state->in + strm->avail_in, state->size - strm->avail_in, &got) == -1) return -1;
94    let s ← ldS state
95    let z ← ldZ strm
96    let (r, got) ← gz_load state (← s.«in».add z.avail_in.toNat) (s.size - z.avail_in)
97    if r == -1 then return -1
98    -- strm->avail_in += got; strm->next_in = state->in;
99    let s ← ldS state
100    updZ strm fun z => { z with avail_in := z.avail_in + got, next_in := s.«in» }
101  return 0
102
103/-- `local int gz_look(gz_statep state)` -/
104def gz_look (state : GzStatePtr) : G Int32 := do
105  let strm := strmOf state
106  let s ← ldS state
107  -- if (state->size == 0) { allocate read buffers and inflate memory }
108  if s.size == 0 then
109    -- state->in = malloc(state->want); state->out = malloc(state->want << 1);
110    let inb ← allocB s.want.toNat
111    updS state fun s => { s with «in» := inb }
112    let s ← ldS state
113    let outb ← allocB (s.want <<< 1).toNat
114    updS state fun s => { s with out := outb }
115    -- if (state->in == NULL || state->out == NULL) { free(state->out); free(state->in); gz_error(...); return -1; }
116    if inb == .null || outb == .null then
117      freeB outb
118      freeB inb
119      gz_error state Z_MEM_ERROR (← strLit "out of memory")
120      return -1
121    -- state->size = state->want;
122    let s ← ldS state
123    updS state fun s => { s with size := s.want }
124    -- state->strm.zalloc = Z_NULL; zfree; opaque; avail_in = 0; next_in = Z_NULL;
125    updZ strm fun z => { z with zalloc := .null, zfree := .null, «opaque» := .null, avail_in := 0, next_in := .null }
126    -- if (inflateInit2(&(state->strm), 15 + 16) != Z_OK) { ... }
127    let ver ← strLit ZLIB_VERSION
128    let r ← inflateInit2_ strm 31 ver 112
129    if r != Z_OK then
130      let s ← ldS state
131      freeB s.out
132      freeB s.«in»
133      updS state fun s => { s with size := 0 }
134      gz_error state Z_MEM_ERROR (← strLit "out of memory")
135      return -1
136  -- if (state->direct == -1 || state->junk == 0) { ... }
137  let s ← ldS state
138  if s.direct == -1 || s.junk == 0 then
139    -- if (state->junk == 0 && strm->avail_in == 0) { ... }
140    if s.junk == 0 && (← ldZ strm).avail_in == 0 then
141      if (← gz_avail state) == -1 then return -1
142      if (← ldZ strm).avail_in == 0 then return 0
143    -- inflateReset(strm); state->how = GZIP; state->junk = state->junk != -1; state->direct = 0;
144    let _ ← inflateReset strm
145    updS state fun s => { s with how := GZIP, junk := if s.junk != -1 then 1 else 0, direct := 0 }
146    return 0
147  -- if (gz_avail(state) == -1) return -1;
148  if (← gz_avail state) == -1 then return -1
149  -- if (strm->avail_in == 0 || (state->again && strm->avail_in < 4)) return 0;
150  let z ← ldZ strm
151  let s ← ldS state
152  if z.avail_in == 0 || (s.again != 0 && z.avail_in < 4) then return 0
153  -- if (strm->avail_in > 3 && next_in[0] == 31 && next_in[1] == 139 && next_in[2] == 8 && next_in[3] < 32) {...}
154  let mut isGz := false
155  if z.avail_in > 3 then
156    if (← index8 z.next_in 0) == 31 then
157      if (← index8 z.next_in 1) == 139 then
158        if (← index8 z.next_in 2) == 8 then
159          if (← index8 z.next_in 3) < 32 then isGz := true
160  if isGz then
161    let _ ← inflateReset strm
162    updS state fun s => { s with how := GZIP, junk := 0, direct := 0 }
163    return 0
164  -- state->x.next = state->out; memcpy(state->x.next, strm->next_in, strm->avail_in);
165  let s ← ldS state
166  updX state fun x => { x with next := s.out }
167  memcpyB s.out z.next_in z.avail_in.toNat
168  -- state->x.have = strm->avail_in; strm->avail_in = 0; state->how = COPY; return 0;
169  updX state fun x => { x with «have» := z.avail_in }
170  updZ strm fun z => { z with avail_in := 0 }
171  updS state fun s => { s with how := GZ_COPY }
172  return 0
173
174structure DecompLoop where
175  ret : Int32
176  brk : Bool
177
178/-- `local int gz_decomp(gz_statep state)` -/
179def gz_decomp (state : GzStatePtr) : G Int32 := do
180  let strm := strmOf state
181  -- int ret = Z_OK; had = strm->avail_out;
182  let had := (← ldZ strm).avail_out
183  let l ← gdoWhile
184    (fun (l : DecompLoop) => do
185      -- if (strm->avail_in == 0 && gz_avail(state) == -1) { ret = state->err; break; }
186      if (← ldZ strm).avail_in == 0 then
187        if (← gz_avail state) == -1 then
188          return { ret := (← ldS state).err, brk := true }
189      -- if (strm->avail_in == 0) { if (!state->again) gz_error(..."unexpected end of file"); break; }
190      if (← ldZ strm).avail_in == 0 then
191        if (← ldS state).again == 0 then
192          gz_error state Z_BUF_ERROR (← strLit "unexpected end of file")
193        return { l with brk := true }
194      -- ret = inflate(strm, Z_NO_FLUSH);
195      let ret ← inflate strm Z_NO_FLUSH
196      -- if (strm->avail_out < had) state->junk = 0;
197      if (← ldZ strm).avail_out < had then updS state fun s => { s with junk := 0 }
198      if ret == Z_STREAM_ERROR || ret == Z_NEED_DICT then
199        gz_error state Z_STREAM_ERROR (← strLit "internal error: inflate stream corrupt")
200        return { ret, brk := true }
201      if ret == Z_MEM_ERROR then
202        gz_error state Z_MEM_ERROR (← strLit "out of memory")
203        return { ret, brk := true }
204      if ret == Z_DATA_ERROR then
205        -- if (state->junk == 1) { trailing garbage is ok }
206        if (← ldS state).junk == 1 then
207          updZ strm fun z => { z with avail_in := 0 }
208          updS state fun s => { s with eof := 1, how := LOOK }
209          return { ret := Z_OK, brk := true }
210        let z ← ldZ strm
211        let msg ← if z.msg == .null then strLit "compressed data error" else pure z.msg
212        gz_error state Z_DATA_ERROR msg
213        return { ret, brk := true }
214      return { l with ret })
215    (fun l => do
216      let z ← ldZ strm
217      pure (!l.brk && z.avail_out != 0 && l.ret != Z_STREAM_END, l))
218    { ret := Z_OK, brk := false }
219  let ret := l.ret
220  -- state->x.have = had - strm->avail_out; state->x.next = strm->next_out - state->x.have;
221  let z ← ldZ strm
222  let hv := had - z.avail_out
223  updX state fun x => { x with «have» := hv }
224  let nx ← z.next_out.add (-(hv.toNat : Int))
225  updX state fun x => { x with next := nx }
226  -- if (ret == Z_STREAM_END) { state->junk = 0; state->how = LOOK; return 0; }
227  if ret == Z_STREAM_END then
228    updS state fun s => { s with junk := 0, how := LOOK }
229    return 0
230  -- return ret != Z_OK ? -1 : 0;
231  return if ret != Z_OK then -1 else 0
232
233/-- `local int gz_fetch(gz_statep state)`. Unpatched: R-2 (upstream PR 1363), see the file comment. The control
234tag of the loop is the result (`some r`: return `r`). -/
235def gz_fetch (state : GzStatePtr) : G Int32 := do
236  let strm := strmOf state
237  -- if (state->err != Z_OK && state->err != Z_BUF_ERROR && !state->again) return -1;
238  let s ← ldS state
239  if s.err != Z_OK && s.err != Z_BUF_ERROR && s.again == 0 then return -1
240  let r ← gdoWhile
241    (fun (r : Option Int32) => do
242      -- switch (state->how)
243      let s ← ldS state
244      if s.how == LOOK then
245        -- case LOOK
246        if (← gz_look state) == -1 then return some (-1)
247        if (← ldS state).how == LOOK then return some 0
248        return none
249      else if s.how == GZ_COPY then
250        -- case COPY: gz_load(state, state->out, state->size << 1, &(state->x.have))
251        let (r, hv) ← gz_load state s.out (s.size <<< 1)
252        updX state fun x => { x with «have» := hv }
253        if r == -1 then return some (-1)
254        -- state->x.next = state->out; return 0;
255        let s ← ldS state
256        updX state fun x => { x with next := s.out }
257        return some 0
258      else if s.how == GZIP then
259        -- case GZIP: strm->avail_out = state->size << 1; strm->next_out = state->out;
260        updZ strm fun z => { z with avail_out := s.size <<< 1, next_out := s.out }
261        if (← gz_decomp state) == -1 then return some (-1)
262        return none
263      else
264        -- default
265        gz_error state Z_STREAM_ERROR (← strLit "state corrupt")
266        return some (-1))
267    (fun r => do
268      if r.isSome then return (false, r)
269      -- while (state->x.have == 0 && (!state->eof || strm->avail_in))
270      let s ← ldS state
271      if s.x.«have» != 0 then return (false, r)
272      if s.eof == 0 then return (true, r)
273      return ((← ldZ strm).avail_in != 0, r))
274    none
275  return r.getD 0
276
277/-- `local void gz_skip_have(gz_statep state)` (R-3/R-4: `x.next += n` also with `n == 0`) -/
278def gz_skip_have (state : GzStatePtr) : M Unit := do
279  let s ← ldS state
280  -- n = GT_OFF(state->x.have) || (z_off64_t)state->x.have > state->skip ? (unsigned)state->skip : state->x.have;
281  let n : UInt32 ← if (← GT_OFF s.x.«have») || u32ToI64 s.x.«have» > s.skip then pure s.skip.toUInt64.toUInt32
282    else pure s.x.«have»
283  -- state->x.have -= n; state->x.next += n; state->x.pos += n; state->skip -= n;
284  updX state fun x => { x with «have» := x.«have» - n }
285  let s ← ldS state
286  let nx ← s.x.next.add n.toNat
287  updX state fun x => { x with next := nx }
288  let s ← ldS state
289  let np ← i64add s.x.pos (u32ToI64 n)
290  updX state fun x => { x with pos := np }
291  let s ← ldS state
292  let sk ← i64sub s.skip (u32ToI64 n)
293  updS state fun s => { s with skip := sk }
294
295/-- `local int gz_skip(gz_statep state)`; the loop tag `some r` means break (`0`) or `return -1`. -/
296def gz_skip (state : GzStatePtr) : G Int32 := do
297  let strm := strmOf state
298  let r ← gdoWhile
299    (fun (_ : Option Int32) => do
300      let s ← ldS state
301      -- if (state->x.have) gz_skip_have(state);
302      if s.x.«have» != 0 then
303        gz_skip_have state
304        return none
305      -- else if (state->eof && state->strm.avail_in == 0) { ... break; }
306      else if s.eof != 0 && (← ldZ strm).avail_in == 0 then
307        if s.how == GZIP && s.err == Z_OK then
308          gz_error state Z_BUF_ERROR (← strLit "unexpected end of file")
309        updS state fun s => { s with skip := 0, past := 1 }
310        return some 0
311      -- else { if (gz_fetch(state) == -1 && state->x.have == 0) return -1; }
312      else
313        if (← gz_fetch state) == -1 && (← ldS state).x.«have» == 0 then return some (-1)
314        return none)
315    (fun r => do
316      if r.isSome then return (false, r)
317      -- while (state->skip)
318      return ((← ldS state).skip != 0, r))
319    none
320  return r.getD 0
321
322structure ReadLoop where
323  got : UInt64
324  len : UInt64
325  buf : BPtr
326  err : Int32
327  brk : Bool
328
329/-- `local z_size_t gz_read(gz_statep state, voidp buf, z_size_t len)`. Unpatched: R-4 (the direct decompression
330into the user's buffer leaves `x.next` pointing into it). -/
331def gz_read (state : GzStatePtr) (buf : BPtr) (len : UInt64) : G UInt64 := do
332  let strm := strmOf state
333  -- if (len == 0) return 0;
334  if len == 0 then return 0
335  -- if (state->skip && gz_skip(state) == -1) return 0;
336  if (← ldS state).skip != 0 then
337    if (← gz_skip state) == -1 then return 0
338  -- got = 0; err = 0; do { ... } while (len && !err);
339  let l ← gdoWhile
340    (fun (l : ReadLoop) => do
341      -- n = (unsigned)-1; if (n > len) n = (unsigned)len;
342      let mut n : UInt32 := 0xFFFFFFFF
343      if n.toUInt64 > l.len then n := l.len.toUInt32
344      let s ← ldS state
345      let mut l := l
346      if s.x.«have» != 0 then
347        -- first just try copying data from the output buffer
348        if s.x.«have» < n then n := s.x.«have»
349        memcpyB l.buf s.x.next n.toNat
350        let nx ← s.x.next.add n.toNat
351        updX state fun x => { x with next := nx, «have» := x.«have» - n }
352        if (← ldS state).err != Z_OK then l := { l with err := -1 }
353      else if s.eof != 0 && (← ldZ strm).avail_in == 0 then
354        -- output buffer empty -- return if we're at the end of the input
355        if s.how == GZIP && s.err == Z_OK then
356          gz_error state Z_BUF_ERROR (← strLit "unexpected end of file")
357        return { l with brk := true }
358      else if s.how == LOOK || n < (s.size <<< 1) then
359        -- need output data -- for small len or new stream load up our output buffer
360        if (← gz_fetch state) == -1 && (← ldS state).x.«have» == 0 then l := { l with err := -1 }
361        return l          -- continue
362      else if s.how == GZ_COPY then
363        -- large len -- read directly into user buffer: err = gz_load(state, buf, n, &n);
364        let (e, nn) ← gz_load state l.buf n
365        l := { l with err := e }
366        n := nn
367      else
368        -- large len -- decompress directly into user buffer
369        updZ strm fun z => { z with avail_out := n, next_out := l.buf }
370        let e ← gz_decomp state
371        l := { l with err := e }
372        n := (← ldS state).x.«have»
373        updX state fun x => { x with «have» := 0 }
374      -- len -= n; buf = (char *)buf + n; got += n; state->x.pos += n;
375      let buf ← l.buf.add n.toNat
376      let s ← ldS state
377      let np ← i64add s.x.pos (u32ToI64 n)
378      updX state fun x => { x with pos := np }
379      return { l with len := l.len - n.toUInt64, buf, got := l.got + n.toUInt64 })
380    (fun l => pure (!l.brk && l.len != 0 && l.err == 0, l))
381    { got := 0, len, buf, err := 0, brk := false }
382  -- if (len && state->eof) state->past = 1;
383  if l.len != 0 && (← ldS state).eof != 0 then updS state fun s => { s with past := 1 }
384  return l.got
385
386/-- `int ZEXPORT gzread(gzFile file, voidp buf, unsigned len)` -/
387def gzread (file : GzFilePtr) (buf : BPtr) (len : UInt32) : G Int32 := do
388  if file.isNone then return -1
389  let state := castState file
390  let s ← ldS state
391  if s.mode != GZ_READ then return -1
392  -- if (state->err != Z_OK && state->err != Z_BUF_ERROR && !state->again && state->x.have == 0) return -1;
393  if s.err != Z_OK && s.err != Z_BUF_ERROR && s.again == 0 && s.x.«have» == 0 then return -1
394  -- if (state->again) gz_error(state, Z_OK, NULL);
395  if s.again != 0 then gz_error state Z_OK .null
396  -- if ((int)len < 0) { ... return -1; }
397  if len.toInt32 < 0 then
398    let s ← ldS state
399    if s.err == Z_OK || s.err == Z_BUF_ERROR then
400      gz_error state Z_STREAM_ERROR (← strLit "request does not fit in an int")
401    return -1
402  -- len = (unsigned)gz_read(state, buf, len);
403  let len : UInt32 := (← gz_read state buf len.toUInt64).toUInt32
404  -- if (len == 0) { ... }
405  if len == 0 then
406    let s ← ldS state
407    if s.err != Z_OK && s.err != Z_BUF_ERROR then return -1
408    if s.again != 0 then
409      gz_error state Z_ERRNO (← zstrerror)
410      return -1
411  return len.toInt32
412
413/-- `z_size_t ZEXPORT gzfread(voidp buf, z_size_t size, z_size_t nitems, gzFile file)` -/
414def gzfread (buf : BPtr) (size nitems : UInt64) (file : GzFilePtr) : G UInt64 := do
415  if file.isNone then return 0
416  let state := castState file
417  let s ← ldS state
418  if s.mode != GZ_READ then return 0
419  if s.err != Z_OK && s.err != Z_BUF_ERROR && s.again == 0 && s.x.«have» == 0 then return 0
420  if s.again != 0 then gz_error state Z_OK .null
421  -- len = nitems * size; if (size && len / size != nitems) { ... return 0; }
422  let len := nitems * size
423  if size != 0 && len / size != nitems then
424    let s ← ldS state
425    if s.err == Z_OK || s.err == Z_BUF_ERROR then
426      gz_error state Z_STREAM_ERROR (← strLit "request does not fit in a size_t")
427    return 0
428  -- return len ? gz_read(state, buf, len) / size : 0;
429  if len != 0 then return (← gz_read state buf len) / size else return 0
430
431/-- `int ZEXPORT gzgetc(gzFile file)` -/
432def gzgetc (file : GzFilePtr) : G Int32 := do
433  -- unsigned char buf[1];
434  if file.isNone then return -1
435  let state := castState file
436  let s ← ldS state
437  if s.mode != GZ_READ then return -1
438  if s.err != Z_OK && s.err != Z_BUF_ERROR && s.again == 0 && s.x.«have» == 0 then return -1
439  if s.again != 0 then gz_error state Z_OK .null
440  -- if (state->x.have) { state->x.have--; state->x.pos++; return *(state->x.next)++; }
441  let s ← ldS state
442  if s.x.«have» != 0 then
443    updX state fun x => { x with «have» := x.«have» - 1 }
444    let np ← i64add s.x.pos 1
445    updX state fun x => { x with pos := np }
446    let s ← ldS state
447    let b ← load8 s.x.next
448    let nx ← s.x.next.add 1
449    updX state fun x => { x with next := nx }
450    return b.toUInt32.toInt32
451  -- return gz_read(state, buf, 1) < 1 ? -1 : buf[0];
452  let buf ← allocLocal 1
453  let got ← gz_read state buf 1
454  let r ← if got < 1 then pure (-1 : Int32) else do pure (← load8 buf).toUInt32.toInt32
455  freeB buf
456  return r
457
458/-- `int ZEXPORT gzgetc_(gzFile file)` -/
459def gzgetc_ (file : GzFilePtr) : G Int32 := gzgetc file
460
461/-- `int ZEXPORT gzungetc(int c, gzFile file)` -/
462def gzungetc (c : Int32) (file : GzFilePtr) : G Int32 := do
463  if file.isNone then return -1
464  let state := castState file
465  let s ← ldS state
466  if s.mode != GZ_READ then return -1
467  -- if (state->how == LOOK && state->x.have == 0) (void)gz_look(state);
468  if s.how == LOOK && s.x.«have» == 0 then
469    let _ ← gz_look state
470  -- if (state->err != Z_OK && state->err != Z_BUF_ERROR && !state->again && state->size == 0) return -1;
471  let s ← ldS state
472  if s.err != Z_OK && s.err != Z_BUF_ERROR && s.again == 0 && s.size == 0 then return -1
473  if s.again != 0 then gz_error state Z_OK .null
474  -- if (state->skip && gz_skip(state) == -1) return -1;
475  if (← ldS state).skip != 0 then
476    if (← gz_skip state) == -1 then return -1
477  -- if (c < 0) return -1;
478  if c < 0 then return -1
479  -- if (state->x.have == 0) { ... return c; }
480  let s ← ldS state
481  if s.x.«have» == 0 then
482    updX state fun x => { x with «have» := 1 }
483    let p ← (← s.out.add (s.size <<< 1).toNat).add (-1)
484    updX state fun x => { x with next := p }
485    store8 p c.toUInt32.toUInt8
486    let s ← ldS state
487    let np ← i64sub s.x.pos 1
488    updX state fun x => { x with pos := np }
489    updS state fun s => { s with past := 0 }
490    return c
491  -- if (state->x.have == (state->size << 1)) { ... return -1; }
492  if s.x.«have» == (s.size <<< 1) then
493    if s.err == Z_OK || s.err == Z_BUF_ERROR then
494      gz_error state Z_DATA_ERROR (← strLit "out of room to push characters")
495    return -1
496  -- if (state->x.next == state->out) { slide output data }
497  if s.x.next == s.out then
498    let src0 ← s.out.add s.x.«have».toNat
499    let dest0 ← s.out.add (s.size <<< 1).toNat
500    -- while (src > state->out) *--dest = *--src;
501    let (_, dest) ← cwhile
502      (fun (st : BPtr × BPtr) => do
503        pure (← Ptr.lt s.out st.1, st))
504      (fun (st : BPtr × BPtr) => do
505        let dest ← st.2.add (-1)
506        let src ← st.1.add (-1)
507        store8 dest (← load8 src)
508        return (src, dest))
509      (src0, dest0)
510    updX state fun x => { x with next := dest }
511  -- state->x.have++; state->x.next--; state->x.next[0] = (unsigned char)c; state->x.pos--; state->past = 0;
512  updX state fun x => { x with «have» := x.«have» + 1 }
513  let s ← ldS state
514  let nx ← s.x.next.add (-1)
515  updX state fun x => { x with next := nx }
516  store8 nx c.toUInt32.toUInt8
517  let s ← ldS state
518  let np ← i64sub s.x.pos 1
519  updX state fun x => { x with pos := np }
520  updS state fun s => { s with past := 0 }
521  return c
522
523structure GetsLoop where
524  left : UInt32
525  buf : BPtr
526  eol : BPtr
527  brk : Bool
528
529/-- `char * ZEXPORT gzgets(gzFile file, char *buf, int len)` -/
530def gzgets (file : GzFilePtr) (buf : BPtr) (len : Int32) : G BPtr := do
531  -- if (file == NULL || buf == NULL || len < 1) return NULL;
532  if file.isNone || buf == .null || len < 1 then return .null
533  let state := castState file
534  let s ← ldS state
535  if s.mode != GZ_READ then return .null
536  if s.err != Z_OK && s.err != Z_BUF_ERROR && s.again == 0 && s.x.«have» == 0 then return .null
537  if s.again != 0 then gz_error state Z_OK .null
538  if (← ldS state).skip != 0 then
539    if (← gz_skip state) == -1 then return .null
540  -- str = buf; left = (unsigned)len - 1;
541  let str := buf
542  let left : UInt32 := len.toUInt32 - 1
543  let mut buf := buf
544  -- if (left) do { ... } while (left && eol == NULL);
545  if left != 0 then
546    let l ← gdoWhile
547      (fun (l : GetsLoop) => do
548        -- if (state->x.have == 0 && gz_fetch(state) == -1 && state->x.have == 0) break;
549        if (← ldS state).x.«have» == 0 then
550          if (← gz_fetch state) == -1 then
551            if (← ldS state).x.«have» == 0 then return { l with brk := true }
552        -- if (state->x.have == 0) { state->past = 1; break; }
553        if (← ldS state).x.«have» == 0 then
554          updS state fun s => { s with past := 1 }
555          return { l with brk := true }
556        -- n = state->x.have > left ? left : state->x.have;
557        let s ← ldS state
558        let mut n : UInt32 := if s.x.«have» > l.left then l.left else s.x.«have»
559        -- eol = memchr(state->x.next, '\n', n);
560        let eol ← memchrB s.x.next 10 n.toNat
561        -- if (eol != NULL) n = (unsigned)(eol - state->x.next) + 1;
562        if eol != .null then
563          let d ← Ptr.diff eol s.x.next
564          n := d.toUInt64.toUInt32 + 1
565        -- memcpy(buf, state->x.next, n); have -= n; next += n; pos += n; left -= n; buf += n;
566        memcpyB l.buf s.x.next n.toNat
567        updX state fun x => { x with «have» := x.«have» - n }
568        let s ← ldS state
569        let nx ← s.x.next.add n.toNat
570        updX state fun x => { x with next := nx }
571        let s ← ldS state
572        let np ← i64add s.x.pos (u32ToI64 n)
573        updX state fun x => { x with pos := np }
574        return { l with left := l.left - n, buf := ← l.buf.add n.toNat, eol })
575      (fun l => pure (!l.brk && l.left != 0 && l.eol == .null, l))
576      { left, buf, eol := .null, brk := false }
577    buf := l.buf
578  -- if (buf == str && len > 1) return NULL; buf[0] = 0; return str;
579  if buf == str && len > 1 then return .null
580  store8 buf 0
581  return str
582
583/-- `int ZEXPORT gzdirect(gzFile file)` -/
584def gzdirect (file : GzFilePtr) : G Int32 := do
585  if file.isNone then return 0
586  let state := castState file
587  let s ← ldS state
588  -- if (state->mode == GZ_READ && state->how == LOOK && state->x.have == 0) { (void)gz_look(state); gz_skip_have(state); }
589  if s.mode == GZ_READ && s.how == LOOK && s.x.«have» == 0 then
590    let _ ← gz_look state
591    gz_skip_have state
592  -- return state->direct == 1;
593  return if (← ldS state).direct == 1 then 1 else 0
594
595/-- `int ZEXPORT gzclose_r(gzFile file)` -/
596def gzclose_r (file : GzFilePtr) : G Int32 := do
597  if file.isNone then return Z_STREAM_ERROR
598  let state := castState file
599  let s ← ldS state
600  if s.mode != GZ_READ then return Z_STREAM_ERROR
601  -- if (state->size) { inflateEnd(&(state->strm)); free(state->out); free(state->in); }
602  if s.size != 0 then
603    let _ ← inflateEnd (strmOf state)
604    freeB s.out
605    freeB s.«in»
606  -- err = state->err == Z_BUF_ERROR ? Z_BUF_ERROR : Z_OK;
607  let err : Int32 := if s.err == Z_BUF_ERROR then Z_BUF_ERROR else Z_OK
608  gz_error state Z_OK .null
609  -- free(state->path); ret = close(state->fd); free(state);
610  let s ← ldS state
611  freeB s.path
612  let ret ← fsClose s.fd
613  freeGzState state
614  return if ret != 0 then Z_ERRNO else err
615
616end Zlib.Gzread