REFERENCE / ZLIB × LEAN
gzread.c.lean
Source snapshot ·
a641249fd952f564 · Source at the matching commit ↗Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.
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