REFERENCE / ZLIB × LEAN
gzlib.c.lean
Source snapshot ·
537b434b9a76b01f · 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.«gzguts.h»
2
3/-!
4# gzlib.c — faithful translation
5
6Source: `gzlib.c` of the verified source (no patch touches it), default x86_64 Linux build: `LSEEK` is `lseek64`
7(`_LARGEFILE64_SOURCE`, `_LFS64_LARGEFILE`), `O_CLOEXEC`, `O_NONBLOCK`, `O_EXCL`, `O_LARGEFILE` are defined
8(`O_LARGEFILE` is 0), `O_BINARY`, `WIDECHAR`, `UNDER_CE`, `NO_GZCOMPRESS` are not. So `gz_strwinerror`, the `-2`
9(wide path) branches and the `#ifndef O_EXCL` block are not compiled.
10
11Open code paths that need a patch in the earlier repository (the translation follows the unpatched C):
12* `gzseek64`: signed overflow with a negative `x.pos` (R-1, upstream PR 1361) is a `Fault.ub`.
13* `gz_reset`: does not write `x.next` (R-3). A fresh `gz_state` has `x.next = NULL`, so `x.next += 0` is `NULL + 0`
14 and does not fault; only R-4 (a dangling `x.next`) can.
15
16File calls go through `Zlib.GzFs` (the model of `open`, `lseek`, `close`, `errno`, `snprintf`).
17-/
18
19namespace Zlib.Gzlib
20open C Zlib.GzFs Zlib.Gzguts
21
22/-- `unsigned ZLIB_INTERNAL gz_intmax(void)` (`INT_MAX` is defined: `return INT_MAX;`) -/
23def gz_intmax : M UInt32 := pure 2147483647
24
25/-- The macro `GT_OFF(x)` of `gzguts.h`: `(sizeof(int) == sizeof(z_off64_t) && (x) > gz_intmax())`. -/
26def GT_OFF (x : UInt32) : M Bool := do
27 if (4 : Nat) == 8 then return decide (x > (← gz_intmax)) else return false
28
29/-- `void ZLIB_INTERNAL gz_error(gz_statep state, int err, const char *msg)` -/
30def gz_error (state : GzStatePtr) (err : Int32) (msg : BPtr) : M Unit := do
31 -- if (state->msg != NULL) { if (state->err != Z_MEM_ERROR) free(state->msg); state->msg = NULL; }
32 let s ← ldS state
33 if s.msg != .null then
34 if s.err != Z_MEM_ERROR then freeB s.msg
35 updS state fun s => { s with msg := .null }
36 -- state->err = err; if (msg == NULL) return;
37 updS state fun s => { s with err := err }
38 if msg == .null then return
39 -- if (err == Z_MEM_ERROR) return;
40 if err == Z_MEM_ERROR then return
41 -- if ((state->msg = malloc(strlen(state->path) + strlen(msg) + 3)) == NULL) { state->err = Z_MEM_ERROR; return; }
42 let s ← ldS state
43 let l1 ← strlenB s.path
44 let l2 ← strlenB msg
45 let m ← allocB (l1 + l2 + 3).toNat
46 updS state fun s => { s with msg := m }
47 if m == .null then
48 updS state fun s => { s with err := Z_MEM_ERROR }
49 return
50 -- (void)snprintf(state->msg, strlen(state->path) + strlen(msg) + 3, "%s%s%s", state->path, ": ", msg);
51 let s ← ldS state
52 let fmt ← strLit "%s%s%s"
53 let sep ← strLit ": "
54 let l1 ← strlenB s.path
55 let l2 ← strlenB msg
56 let _ ← vsnprintf s.msg (l1 + l2 + 3) fmt [.str s.path, .str sep, .str msg]
57
58/-- `local void gz_reset(gz_statep state)`. Does not write `x.next` (R-3: the earlier repository's `ub.patch`
59hunk `state->x.next = Z_NULL;` is not applied; a fresh state has `x.next = NULL` in the model). -/
60def gz_reset (state : GzStatePtr) : M Unit := do
61 -- state->x.have = 0; state->past = 0;
62 updX state fun x => { x with «have» := 0 }
63 updS state fun s => { s with past := 0 }
64 -- if (state->mode == GZ_READ) { eof = 0; how = LOOK; junk = -1; } else state->reset = 0;
65 let s ← ldS state
66 if s.mode == GZ_READ then
67 updS state fun s => { s with eof := 0, how := LOOK, junk := -1 }
68 else
69 updS state fun s => { s with reset := 0 }
70 -- state->again = 0; state->skip = 0;
71 updS state fun s => { s with again := 0, skip := 0 }
72 -- gz_error(state, Z_OK, NULL);
73 gz_error state Z_OK .null
74 -- state->x.pos = 0; state->strm.avail_in = 0;
75 updX state fun x => { x with pos := 0 }
76 updZ (strmOf state) fun z => { z with avail_in := 0 }
77
78/-- Loop-carried locals of the mode loop of `gz_open`; `done` is the control tag for `return NULL`. -/
79structure ModeLoop where
80 mode : BPtr
81 oflag : Int32
82 exclusive : Int32
83 done : Bool
84
85/-- `local gzFile gz_open(const void *path, int fd, const char *mode)` -/
86def gz_open (path : BPtr) (fd : Int32) (mode : BPtr) : G GzFilePtr := do
87 -- int oflag = 0; int exclusive = 0;
88 -- if (path == NULL || mode == NULL) return NULL;
89 if path == .null || mode == .null then return none
90 -- state = (gz_statep)malloc(sizeof(gz_state)); if (state == NULL) return NULL;
91 let state ← allocGzState
92 if state.isNone then return none
93 -- state->size = 0; state->want = GZBUFSIZE; state->err = Z_OK; state->msg = NULL;
94 updS state fun s => { s with size := 0, want := GZBUFSIZE.toUInt32, err := Z_OK, msg := .null }
95 -- state->mode = GZ_NONE; level = Z_DEFAULT_COMPRESSION; strategy = Z_DEFAULT_STRATEGY; direct = 0;
96 updS state fun s => { s with mode := GZ_NONE, level := Z_DEFAULT_COMPRESSION, strategy := Z_DEFAULT_STRATEGY,
97 direct := 0 }
98 -- while (*mode) { ... mode++; }
99 let ml ← gwhile
100 (fun (l : ModeLoop) => do
101 let c ← load8 l.mode
102 return (c != 0 && !l.done, l))
103 (fun (l : ModeLoop) => do
104 let c : Int32 := (← load8 l.mode).toInt8.toInt32
105 let mut l := l
106 if c ≥ 48 && c ≤ 57 then
107 -- state->level = *mode - '0';
108 updS state fun s => { s with level := c - 48 }
109 else if c == 114 then -- 'r'
110 updS state fun s => { s with mode := GZ_READ }
111 else if c == 119 then -- 'w'
112 updS state fun s => { s with mode := GZ_WRITE }
113 else if c == 97 then -- 'a'
114 updS state fun s => { s with mode := GZ_APPEND }
115 else if c == 43 then -- '+': can't read and write at the same time
116 freeGzState state
117 l := { l with done := true }
118 else if c == 98 then -- 'b'
119 pure ()
120 else if c == 101 then -- 'e'
121 l := { l with oflag := l.oflag ||| O_CLOEXEC }
122 else if c == 120 then -- 'x'
123 l := { l with exclusive := 1 }
124 else if c == 102 then -- 'f'
125 updS state fun s => { s with strategy := Z_FILTERED }
126 else if c == 104 then -- 'h'
127 updS state fun s => { s with strategy := Z_HUFFMAN_ONLY }
128 else if c == 82 then -- 'R'
129 updS state fun s => { s with strategy := Z_RLE }
130 else if c == 70 then -- 'F'
131 updS state fun s => { s with strategy := Z_FIXED }
132 else if c == 71 then -- 'G'
133 updS state fun s => { s with direct := -1 }
134 else if c == 78 then -- 'N'
135 l := { l with oflag := l.oflag ||| O_NONBLOCK }
136 else if c == 84 then -- 'T'
137 updS state fun s => { s with direct := 1 }
138 else pure () -- default: ignore
139 if !l.done then l := { l with mode := ← l.mode.add 1 }
140 return l)
141 { mode, oflag := 0, exclusive := 0, done := false }
142 if ml.done then return none
143 let oflag0 := ml.oflag
144 let exclusive := ml.exclusive
145 -- if (state->mode == GZ_NONE) { free(state); return NULL; }
146 let s ← ldS state
147 if s.mode == GZ_NONE then
148 freeGzState state
149 return none
150 -- direct is 0, 1 if "T", or -1 if "G"
151 if s.mode == GZ_READ then
152 if s.direct == 1 then
153 freeGzState state
154 return none
155 if s.direct == 0 then
156 updS state fun s => { s with direct := 1 }
157 else if s.direct == -1 then
158 freeGzState state
159 return none
160 -- len = strlen((const char *)path); state->path = (char *)malloc(len + 1);
161 let len ← strlenB path
162 let p ← allocB (len + 1).toNat
163 updS state fun s => { s with path := p }
164 if p == .null then
165 freeGzState state
166 return none
167 -- (void)snprintf(state->path, len + 1, "%s", (const char *)path);
168 let fmt ← strLit "%s"
169 let _ ← vsnprintf p (len + 1) fmt [.str path]
170 -- compute the flags for open()
171 let s ← ldS state
172 let oflag : Int32 := oflag0 ||| (O_LARGEFILE |||
173 (if s.mode == GZ_READ then 0
174 else (O_WRONLY ||| O_CREAT ||| (if exclusive != 0 then O_EXCL else 0) |||
175 (if s.mode == GZ_WRITE then O_TRUNC else O_APPEND))))
176 -- open the file with the appropriate flags (or just use fd)
177 if fd == -1 then
178 -- state->fd = open((const char *)path, oflag, 0666);
179 let name ← cstring path
180 let r ← fsOpen name oflag
181 updS state fun s => { s with fd := r }
182 else
183 -- if (oflag & O_NONBLOCK) fcntl(fd, F_SETFL, fcntl(fd, F_GETFL) | O_NONBLOCK);
184 if oflag &&& O_NONBLOCK != 0 then fsFcntl fd
185 -- if (oflag & O_CLOEXEC) fcntl(fd, F_SETFD, fcntl(fd, F_GETFD) | FD_CLOEXEC);
186 if oflag &&& O_CLOEXEC != 0 then fsFcntl fd
187 updS state fun s => { s with fd := fd }
188 -- if (state->fd == -1) { free(state->path); free(state); return NULL; }
189 let s ← ldS state
190 if s.fd == -1 then
191 freeB s.path
192 freeGzState state
193 return none
194 -- if (state->mode == GZ_APPEND) { LSEEK(state->fd, 0, SEEK_END); state->mode = GZ_WRITE; }
195 if s.mode == GZ_APPEND then
196 let _ ← fsLseek s.fd 0 SEEK_END
197 updS state fun s => { s with mode := GZ_WRITE }
198 -- if (state->mode == GZ_READ) { state->start = LSEEK(state->fd, 0, SEEK_CUR); if (state->start == -1) state->start = 0; }
199 let s ← ldS state
200 if s.mode == GZ_READ then
201 let st ← fsLseek s.fd 0 SEEK_CUR
202 updS state fun s => { s with start := st }
203 if st == -1 then updS state fun s => { s with start := 0 }
204 -- gz_reset(state); return (gzFile)state;
205 gz_reset state
206 return castFile state
207
208/-- `gzFile ZEXPORT gzopen(const char *path, const char *mode)` -/
209def gzopen (path mode : BPtr) : G GzFilePtr := gz_open path (-1) mode
210
211/-- `gzFile ZEXPORT gzopen64(const char *path, const char *mode)` -/
212def gzopen64 (path mode : BPtr) : G GzFilePtr := gz_open path (-1) mode
213
214/-- `gzFile ZEXPORT gzdopen(int fd, const char *mode)` -/
215def gzdopen (fd : Int32) (mode : BPtr) : G GzFilePtr := do
216 -- if (fd < 0 || (path = (char *)malloc(7 + 3 * sizeof(int))) == NULL) return NULL;
217 if fd < 0 then return none
218 let path ← allocB (7 + 3 * 4)
219 if path == .null then return none
220 -- (void)snprintf(path, 7 + 3 * sizeof(int), "<fd:%d>", fd);
221 let fmt ← strLit "<fd:%d>"
222 let _ ← vsnprintf path (7 + 3 * 4) fmt [.int fd]
223 -- gz = gz_open(path, fd, mode); free(path); return gz;
224 let gz ← gz_open path fd mode
225 freeB path
226 return gz
227
228/-- `int ZEXPORT gzbuffer(gzFile file, unsigned size)` -/
229def gzbuffer (file : GzFilePtr) (size : UInt32) : M Int32 := do
230 -- if (file == NULL) return -1;
231 if file.isNone then return -1
232 let state := castState file
233 let s ← ldS state
234 -- if (state->mode != GZ_READ && state->mode != GZ_WRITE) return -1;
235 if s.mode != GZ_READ && s.mode != GZ_WRITE then return -1
236 -- if (state->size != 0) return -1;
237 if s.size != 0 then return -1
238 -- if ((size << 1) < size) return -1;
239 if (size <<< 1) < size then return -1
240 -- if (size < 8) size = 8; state->want = size; return 0;
241 let size := if size < 8 then 8 else size
242 updS state fun s => { s with want := size }
243 return 0
244
245/-- `int ZEXPORT gzrewind(gzFile file)` -/
246def gzrewind (file : GzFilePtr) : G Int32 := do
247 if file.isNone then return -1
248 let state := castState file
249 let s ← ldS state
250 -- if (state->mode != GZ_READ || (state->err != Z_OK && state->err != Z_BUF_ERROR)) return -1;
251 if s.mode != GZ_READ || (s.err != Z_OK && s.err != Z_BUF_ERROR) then return -1
252 -- if (LSEEK(state->fd, state->start, SEEK_SET) == -1) return -1;
253 if (← fsLseek s.fd s.start SEEK_SET) == -1 then return -1
254 gz_reset state
255 return 0
256
257/-- `z_off64_t ZEXPORT gzseek64(gzFile file, z_off64_t offset, int whence)`. Unpatched: signed overflow after a
258`gzungetc()` right after `gzopen()` (R-1, upstream PR 1361) is `Fault.ub`. -/
259def gzseek64 (file : GzFilePtr) (offset : Int64) (whence : Int32) : G Int64 := do
260 if file.isNone then return -1
261 let state := castState file
262 let s ← ldS state
263 if s.mode != GZ_READ && s.mode != GZ_WRITE then return -1
264 -- check that there's no error
265 if s.err != Z_OK && s.err != Z_BUF_ERROR then return -1
266 -- can only seek from start or relative to current position
267 if whence != SEEK_SET && whence != SEEK_CUR then return -1
268 -- pos = whence == SEEK_SET ? 0 : state->x.pos + (state->past ? 0 : state->skip);
269 let mut pos : Int64 ← if whence == SEEK_SET then pure 0
270 else i64add s.x.pos (if s.past != 0 then 0 else s.skip)
271 -- if (offset > GZ_OFF_MAX - pos) return -1;
272 if offset > (← i64sub GZ_OFF_MAX pos) then return -1
273 -- if (offset < -pos) return -1;
274 if offset < (← i64neg pos) then return -1
275 -- pos += offset;
276 pos ← i64add pos offset
277 -- if (state->mode == GZ_READ && state->how == COPY) { ... }
278 if s.mode == GZ_READ && s.how == GZ_COPY then
279 let d ← i64sub (← i64sub pos s.x.pos) (u32ToI64 s.x.«have»)
280 let ret ← fsLseek s.fd d SEEK_CUR
281 if ret == -1 then return -1
282 updX state fun x => { x with «have» := 0 }
283 updS state fun s => { s with eof := 0, past := 0, skip := 0 }
284 gz_error state Z_OK .null
285 updZ (strmOf state) fun z => { z with avail_in := 0 }
286 updX state fun x => { x with pos := pos }
287 return pos
288 -- if (pos < state->x.pos) { if (state->mode != GZ_READ) return -1; if (gzrewind(file) == -1) return -1; }
289 let s ← ldS state
290 if pos < s.x.pos then
291 if s.mode != GZ_READ then return -1
292 if (← gzrewind file) == -1 then return -1
293 -- offset = pos - state->x.pos;
294 let s ← ldS state
295 let mut offset ← i64sub pos s.x.pos
296 -- if (state->mode == GZ_READ) { ... }
297 if s.mode == GZ_READ then
298 let s ← ldS state
299 -- n = GT_OFF(state->x.have) || (z_off64_t)state->x.have > offset ? (unsigned)offset : state->x.have;
300 let n : UInt32 ← if (← GT_OFF s.x.«have») || u32ToI64 s.x.«have» > offset then pure offset.toUInt64.toUInt32
301 else pure s.x.«have»
302 -- state->x.have -= n; state->x.next += n; state->x.pos += n; offset -= n;
303 updX state fun x => { x with «have» := x.«have» - n }
304 let s ← ldS state
305 let nx ← s.x.next.add n.toNat
306 updX state fun x => { x with next := nx }
307 let s ← ldS state
308 let np ← i64add s.x.pos (u32ToI64 n)
309 updX state fun x => { x with pos := np }
310 offset ← i64sub offset (u32ToI64 n)
311 -- state->skip = offset; return pos;
312 updS state fun s => { s with skip := offset }
313 return pos
314
315/-- `z_off_t ZEXPORT gzseek(gzFile file, z_off_t offset, int whence)` (`z_off_t` is `long`) -/
316def gzseek (file : GzFilePtr) (offset : Int64) (whence : Int32) : G Int64 := do
317 -- ret = gzseek64(file, (z_off64_t)offset, whence);
318 let ret ← gzseek64 file offset whence
319 -- return ret == (z_off_t)ret ? (z_off_t)ret : -1;
320 return if ret == ret then ret else -1
321
322/-- `z_off64_t ZEXPORT gztell64(gzFile file)` -/
323def gztell64 (file : GzFilePtr) : M Int64 := do
324 if file.isNone then return -1
325 let state := castState file
326 let s ← ldS state
327 if s.mode != GZ_READ && s.mode != GZ_WRITE then return -1
328 -- return state->x.pos + (state->past ? 0 : state->skip);
329 i64add s.x.pos (if s.past != 0 then 0 else s.skip)
330
331/-- `z_off_t ZEXPORT gztell(gzFile file)` -/
332def gztell (file : GzFilePtr) : M Int64 := do
333 let ret ← gztell64 file
334 return if ret == ret then ret else -1
335
336/-- `z_off64_t ZEXPORT gzoffset64(gzFile file)` -/
337def gzoffset64 (file : GzFilePtr) : G Int64 := do
338 if file.isNone then return -1
339 let state := castState file
340 let s ← ldS state
341 if s.mode != GZ_READ && s.mode != GZ_WRITE then return -1
342 -- offset = LSEEK(state->fd, 0, SEEK_CUR); if (offset == -1) return -1;
343 let mut offset ← fsLseek s.fd 0 SEEK_CUR
344 if offset == -1 then return -1
345 -- if (state->mode == GZ_READ) offset -= state->strm.avail_in;
346 if s.mode == GZ_READ then
347 let z ← ldZ (strmOf state)
348 offset ← i64sub offset (u32ToI64 z.avail_in)
349 return offset
350
351/-- `z_off_t ZEXPORT gzoffset(gzFile file)` -/
352def gzoffset (file : GzFilePtr) : G Int64 := do
353 let ret ← gzoffset64 file
354 return if ret == ret then ret else -1
355
356/-- `int ZEXPORT gzeof(gzFile file)` -/
357def gzeof (file : GzFilePtr) : M Int32 := do
358 if file.isNone then return 0
359 let state := castState file
360 let s ← ldS state
361 if s.mode != GZ_READ && s.mode != GZ_WRITE then return 0
362 -- return state->mode == GZ_READ ? state->past : 0;
363 return if s.mode == GZ_READ then s.past else 0
364
365/-- `const char * ZEXPORT gzerror(gzFile file, int *errnum)`. `errnum` is a pointer to a 4-byte block
366(little-endian `int`, see `gzguts.h.lean`). -/
367def gzerror (file : GzFilePtr) (errnum : BPtr) : M BPtr := do
368 if file.isNone then return .null
369 let state := castState file
370 let s ← ldS state
371 if s.mode != GZ_READ && s.mode != GZ_WRITE then return .null
372 -- if (errnum != NULL) *errnum = state->err;
373 if errnum != .null then store32 errnum s.err
374 -- return state->err == Z_MEM_ERROR ? "out of memory" : (state->msg == NULL ? "" : state->msg);
375 if s.err == Z_MEM_ERROR then strLit "out of memory"
376 else if s.msg == .null then strLit ""
377 else pure s.msg
378
379/-- `void ZEXPORT gzclearerr(gzFile file)` -/
380def gzclearerr (file : GzFilePtr) : M Unit := do
381 if file.isNone then return
382 let state := castState file
383 let s ← ldS state
384 if s.mode != GZ_READ && s.mode != GZ_WRITE then return
385 -- if (state->mode == GZ_READ) { state->eof = 0; state->past = 0; }
386 if s.mode == GZ_READ then
387 updS state fun s => { s with eof := 0, past := 0 }
388 gz_error state Z_OK .null
389
390end Zlib.Gzlib