REFERENCE / ZLIB × LEAN
inftrees.c.lean
Source snapshot ·
0cf26d03d47fbbe8 · 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.Runtime.Alloc
2import ZlibF.Runtime.Tables
3import ZlibF.Zlib.«inffixed.h»
4
5/-!
6# inftrees.c — faithful translation
7
8Source: `inftrees.c` (with `inftrees.h`, `inffixed.h`), default x86_64 Linux build. `MAKEFIXED`, `BUILDFIXED`,
9`Z_ONCE` are undefined, so `buildtables`, `z_once` and `main` are dead and `inflate_fixed` uses the tables of
10`inffixed.h` (`inffixed.h.lean`, copied entry for entry). `inflate_copyright` is a `const char[]` that nothing reads;
11it is not translated.
12
13Decisions (the C line of each is in the code):
14
15* `unsigned short FAR *lens`, `*work` are `WPtr`. `code FAR * FAR *table` and `unsigned FAR *bits` point to fields of
16 `inflate_state` (`&state->next`, `&state->lenbits`, ...), which the schema does not model: the function takes their
17 values and returns the new ones, `(ret, table', bits')`. On `return -1` and `return 1` the C stores nothing through
18 them, so the inputs are returned; table entries written so far stay written.
19* `count[16]`, `offs[16]` are local `unsigned short` arrays: `Array UInt16`, indexed with a check (an index outside
20 0..15 is a fault; the C says "assumes, but does not check" that every `lens[i] <= 15`).
21* `lbase`, `lext`, `dbase`, `dext` are function-local `static const` tables that are only indexed: `Array UInt16`
22 constants. `base` and `extra` are NULL for `CODES`: the empty array, so a read through them is a fault.
23* Signed `int` arithmetic (`left`) is checked; shifts fault for a count outside the width of the type
24 (and a signed `1 << curr` faults when the result does not fit in `int`).
25* `min` is reused at C line "min = fill" as in the C: one variable, new meaning.
26-/
27
28namespace Zlib.Inftrees
29open C
30
31/-! ### Small checked operations -/
32
33/-- A signed `int` result: a fault if it does not fit. -/
34def chk32 (v : Int) : M Int32 :=
35 if -2147483648 ≤ v ∧ v ≤ 2147483647 then pure (Int32.ofInt v) else ub "signed integer overflow"
36
37/-- `x << n` for `unsigned`: undefined if `n >= 32`. -/
38def shl32 (x n : UInt32) : M UInt32 :=
39 if n < 32 then pure (x <<< n) else ub "shift count out of range"
40
41/-- `x >> n` for `unsigned`: undefined if `n >= 32`. -/
42def shr32 (x n : UInt32) : M UInt32 :=
43 if n < 32 then pure (x >>> n) else ub "shift count out of range"
44
45/-- `1 << n` for `int`: undefined if `n >= 32` or the result is not representable (`n = 31`). -/
46def shl1i32 (n : UInt32) : M Int32 :=
47 if n < 31 then pure (1 <<< n.toInt32) else ub "signed shift out of range"
48
49/-- `a[i]` for a local array. -/
50def geta (a : Array UInt16) (i : Nat) : M UInt16 :=
51 match a[i]? with
52 | some v => pure v
53 | none => ub "array index outside its object"
54
55/-- `a[i] = v` for a local array. -/
56def seta (a : Array UInt16) (i : Nat) (v : UInt16) : M (Array UInt16) :=
57 if i < a.size then pure (a.set! i v) else ub "array index outside its object"
58
59/-- `p[i] = v` for a pointer into an array of `code`. -/
60def storeCode (p : CodePtr) (i : Nat) (v : Code) : M Unit := do
61 let q ← p.add i
62 Ptr.store q v
63
64/-! ### Tables -/
65
66def MAXBITS : UInt32 := 15
67
68/-- `static const unsigned short lbase[31]` -/
69def lbase : Array UInt16 :=
70 #[3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 15, 17, 19, 23, 27, 31,
71 35, 43, 51, 59, 67, 83, 99, 115, 131, 163, 195, 227, 258, 0, 0]
72/-- `static const unsigned short lext[31]` -/
73def lext : Array UInt16 :=
74 #[16, 16, 16, 16, 16, 16, 16, 16, 17, 17, 17, 17, 18, 18, 18, 18,
75 19, 19, 19, 19, 20, 20, 20, 20, 21, 21, 21, 21, 16, 68, 193]
76/-- `static const unsigned short dbase[32]` -/
77def dbase : Array UInt16 :=
78 #[1, 2, 3, 4, 5, 7, 9, 13, 17, 25, 33, 49, 65, 97, 129, 193,
79 257, 385, 513, 769, 1025, 1537, 2049, 3073, 4097, 6145,
80 8193, 12289, 16385, 24577, 0, 0]
81/-- `static const unsigned short dext[32]` -/
82def dext : Array UInt16 :=
83 #[16, 16, 16, 16, 17, 17, 18, 18, 19, 19, 20, 20, 21, 21, 22, 22,
84 23, 23, 24, 24, 25, 25, 26, 26, 27, 27,
85 28, 28, 29, 29, 64, 64]
86
87/-- The `Statics` with the contents that `inftrees.c` fixes: `lenfix` and `distfix` (from `inffixed.h`). -/
88def initStatics (s : Statics) : Statics :=
89 { s with lenfix := Zlib.InffixedH.lenfix, distfix := Zlib.InffixedH.distfix }
90
91/-! ### `inflate_table` -/
92
93/-- Loop-carried locals of the main loop of `inflate_table` (`for (;;)`). `exit` is 0 while the loop runs, 1 after
94the `break`, 2 after `return 1`. -/
95structure TS where
96 huff : UInt32
97 sym : UInt32
98 len : UInt32
99 curr : UInt32
100 drop : UInt32
101 low : UInt32
102 used : UInt32
103 min : UInt32
104 fill : UInt32
105 incr : UInt32
106 mask : UInt32
107 left : Int32
108 next : CodePtr
109 here : Code
110 count : Array UInt16
111 exit : UInt8
112
113/-- What the main loop reads and never changes. -/
114structure Ctx where
115 type : UInt32
116 lens : WPtr
117 work : WPtr
118 table : CodePtr
119 root : UInt32
120 max : UInt32
121 base : Array UInt16
122 extra : Array UInt16
123 match_ : UInt32
124
125/-- `(type == LENS && used > ENOUGH_LENS) || (type == DISTS && used > ENOUGH_DISTS)` -/
126def tooBig (type used : UInt32) : Bool :=
127 (type == LENS && used > ENOUGH_LENS.toUInt32) || (type == DISTS && used > ENOUGH_DISTS.toUInt32)
128
129/-- One pass of the body of the `for (;;)` loop of `inflate_table`. -/
130def buildStep (c : Ctx) (s : TS) : M TS := do
131 let mut s := s
132 -- here.bits = (unsigned char)(len - drop);
133 s := { s with here := { s.here with bits := (s.len - s.drop).toUInt8 } }
134 -- if (work[sym] + 1U < match) {
135 let w ← c.work.index s.sym.toNat
136 if w.toUInt32 + 1 < c.match_ then
137 -- here.op = (unsigned char)0; here.val = work[sym];
138 s := { s with here := { s.here with op := 0 } }
139 let w ← c.work.index s.sym.toNat
140 s := { s with here := { s.here with val := w } }
141 else
142 -- else if (work[sym] >= match) {
143 let w ← c.work.index s.sym.toNat
144 if w.toUInt32 ≥ c.match_ then
145 -- here.op = (unsigned char)(extra[work[sym] - match]);
146 let w ← c.work.index s.sym.toNat
147 let e ← geta c.extra (w.toUInt32 - c.match_).toNat
148 s := { s with here := { s.here with op := e.toUInt8 } }
149 -- here.val = base[work[sym] - match];
150 let w ← c.work.index s.sym.toNat
151 let b ← geta c.base (w.toUInt32 - c.match_).toNat
152 s := { s with here := { s.here with val := b } }
153 else
154 -- here.op = (unsigned char)(32 + 64); here.val = 0; /* end of block */
155 s := { s with here := { s.here with op := 96, val := 0 } }
156 -- incr = 1U << (len - drop); fill = 1U << curr; min = fill;
157 let incr ← shl32 1 (s.len - s.drop)
158 let fill ← shl32 1 s.curr
159 s := { s with incr, fill, min := fill }
160 -- do { fill -= incr; next[(huff >> drop) + fill] = here; } while (fill != 0);
161 s ← cdoWhile
162 (fun s => do
163 let fill := s.fill - s.incr
164 let hd ← shr32 s.huff s.drop
165 storeCode s.next (hd + fill).toNat s.here
166 pure { s with fill })
167 (fun s => pure (s.fill != 0, s)) s
168 -- incr = 1U << (len - 1);
169 let incr ← shl32 1 (s.len - 1)
170 s := { s with incr }
171 -- while (huff & incr) incr >>= 1;
172 s ← cwhile (fun s => pure (s.huff &&& s.incr != 0, s)) (fun s => pure { s with incr := s.incr >>> 1 }) s
173 -- if (incr != 0) { huff &= incr - 1; huff += incr; } else huff = 0;
174 if s.incr != 0 then
175 s := { s with huff := s.huff &&& (s.incr - 1) }
176 s := { s with huff := s.huff + s.incr }
177 else
178 s := { s with huff := 0 }
179 -- sym++;
180 s := { s with sym := s.sym + 1 }
181 -- if (--(count[len]) == 0) {
182 let cl ← geta s.count s.len.toNat
183 let cl := cl - 1
184 s := { s with count := ← seta s.count s.len.toNat cl }
185 if cl == 0 then
186 -- if (len == max) break;
187 if s.len == c.max then
188 return { s with exit := 1 }
189 -- len = lens[work[sym]];
190 let w ← c.work.index s.sym.toNat
191 let l ← c.lens.index w.toNat
192 s := { s with len := l.toUInt32 }
193 -- if (len > root && (huff & mask) != low) {
194 if s.len > c.root && (s.huff &&& s.mask) != s.low then
195 -- if (drop == 0) drop = root;
196 if s.drop == 0 then s := { s with drop := c.root }
197 -- next += min; /* here min is 1 << curr */
198 s := { s with next := ← s.next.add s.min.toNat }
199 -- curr = len - drop; left = (int)(1 << curr);
200 s := { s with curr := s.len - s.drop }
201 s := { s with left := ← shl1i32 s.curr }
202 -- while (curr + drop < max) { left -= count[curr + drop]; if (left <= 0) break; curr++; left <<= 1; }
203 let (curr, left, _) ← cwhile
204 (fun (curr, left, brk) => pure (!brk && curr + s.drop < c.max, (curr, left, brk)))
205 (fun (curr, left, brk) => do
206 let cc ← geta s.count (curr + s.drop).toNat
207 let left ← chk32 (left.toInt - cc.toNat)
208 if left ≤ 0 then pure (curr, left, true)
209 else
210 let curr := curr + 1
211 let left ← chk32 (left.toInt * 2)
212 pure (curr, left, brk))
213 (s.curr, s.left, false)
214 s := { s with curr, left }
215 -- used += 1U << curr;
216 let u ← shl32 1 s.curr
217 s := { s with used := s.used + u }
218 -- if ((type == LENS && used > ENOUGH_LENS) || (type == DISTS && used > ENOUGH_DISTS)) return 1;
219 if tooBig c.type s.used then
220 return { s with exit := 2 }
221 -- low = huff & mask;
222 s := { s with low := s.huff &&& s.mask }
223 -- (*table)[low].op = (unsigned char)curr;
224 let q ← c.table.add s.low.toNat
225 let e ← q.load
226 q.store { e with op := s.curr.toUInt8 }
227 -- (*table)[low].bits = (unsigned char)root;
228 let q ← c.table.add s.low.toNat
229 let e ← q.load
230 q.store { e with bits := c.root.toUInt8 }
231 -- (*table)[low].val = (unsigned short)(next - *table);
232 let d ← s.next.diff c.table
233 let q ← c.table.add s.low.toNat
234 let e ← q.load
235 q.store { e with val := d.toUInt64.toUInt16 }
236 pure s
237
238/-- `int ZLIB_INTERNAL inflate_table(codetype type, unsigned short FAR *lens, unsigned codes, code FAR * FAR *table,
239unsigned FAR *bits, unsigned short FAR *work)`
240
241`table` and `bits` are passed as the values `*table`, `*bits`; the result is `(return value, *table, *bits)` after
242the call. -/
243def inflate_table (type : UInt32) (lens : WPtr) (codes : UInt32) (table : CodePtr) (bits : UInt32) (work : WPtr) :
244 M (Int32 × CodePtr × UInt32) := do
245 -- unsigned short count[MAXBITS+1]; unsigned short offs[MAXBITS+1]; (uninitialised in C; count is cleared below)
246 let count : Array UInt16 := Array.replicate 16 0
247 let offs : Array UInt16 := Array.replicate 16 0
248 -- for (len = 0; len <= MAXBITS; len++) count[len] = 0;
249 let (_, count) ← cwhile (fun (len, count) => pure (len ≤ MAXBITS, (len, count)))
250 (fun (len, count) => do pure (len + 1, ← seta count len.toNat 0)) ((0 : UInt32), count)
251 -- for (sym = 0; sym < codes; sym++) count[lens[sym]]++;
252 let (_, count) ← cwhile (fun (sym, count) => pure (sym < codes, (sym, count)))
253 (fun (sym, count) => do
254 let l ← lens.index sym.toNat
255 let c ← geta count l.toNat
256 pure (sym + 1, ← seta count l.toNat (c + 1))) ((0 : UInt32), count)
257 -- root = *bits;
258 let mut root := bits
259 -- for (max = MAXBITS; max >= 1; max--) if (count[max] != 0) break;
260 let (max, _) ← cwhile (fun (max, brk) => pure (!brk && max ≥ 1, (max, brk)))
261 (fun (max, brk) => do
262 if (← geta count max.toNat) != 0 then pure (max, true) else pure (max - 1, brk)) (MAXBITS, false)
263 -- if (root > max) root = max;
264 if root > max then root := max
265 -- if (max == 0) { /* no symbols to code at all */
266 if max == 0 then
267 -- here.op = 64; here.bits = 1; here.val = 0;
268 let here : Code := ⟨64, 1, 0⟩
269 -- *(*table)++ = here; *(*table)++ = here;
270 Ptr.store table here
271 let table ← table.add 1
272 Ptr.store table here
273 let table ← table.add 1
274 -- *bits = 1; return 0;
275 return (0, table, 1)
276 -- for (min = 1; min < max; min++) if (count[min] != 0) break;
277 let (min, _) ← cwhile (fun (min, brk) => pure (!brk && min < max, (min, brk)))
278 (fun (min, brk) => do
279 if (← geta count min.toNat) != 0 then pure (min, true) else pure (min + 1, brk)) ((1 : UInt32), false)
280 -- if (root < min) root = min;
281 if root < min then root := min
282 -- left = 1; for (len = 1; len <= MAXBITS; len++) { left <<= 1; left -= count[len]; if (left < 0) return -1; }
283 let (left, bad, _) ← cwhile (fun (left, bad, len) => pure (!bad && len ≤ MAXBITS, (left, bad, len)))
284 (fun (left, bad, len) => do
285 if left < 0 then ub "left shift of a negative value" else
286 let left ← chk32 (left.toInt * 2)
287 let cc ← geta count len.toNat
288 let left ← chk32 (left.toInt - cc.toNat)
289 if left < 0 then pure (left, true, len) else pure (left, bad, len + 1)) ((1 : Int32), false, (1 : UInt32))
290 -- /* over-subscribed */ return -1;
291 if bad then return (-1, table, bits)
292 -- if (left > 0 && (type == CODES || max != 1)) return -1; /* incomplete set */
293 if left > 0 && (type == CODES || max != 1) then return (-1, table, bits)
294 -- offs[1] = 0;
295 let offs ← seta offs 1 0
296 -- for (len = 1; len < MAXBITS; len++) offs[len + 1] = offs[len] + count[len];
297 let (_, offs) ← cwhile (fun (len, offs) => pure (len < MAXBITS, (len, offs)))
298 (fun (len, offs) => do
299 let a ← geta offs len.toNat
300 let b ← geta count len.toNat
301 pure (len + 1, ← seta offs (len + 1).toNat (a + b))) ((1 : UInt32), offs)
302 -- for (sym = 0; sym < codes; sym++) if (lens[sym] != 0) work[offs[lens[sym]]++] = (unsigned short)sym;
303 let (_, offs) ← cwhile (fun (sym, offs) => pure (sym < codes, (sym, offs)))
304 (fun (sym, offs) => do
305 let l ← lens.index sym.toNat
306 if l != 0 then
307 let l ← lens.index sym.toNat
308 let o ← geta offs l.toNat
309 let offs ← seta offs l.toNat (o + 1)
310 let q ← work.add o.toNat
311 Ptr.store q sym.toUInt16
312 pure (sym + 1, offs)
313 else pure (sym + 1, offs)) ((0 : UInt32), offs)
314 -- switch (type) { case CODES: match = 20; break; case LENS: base = lbase; extra = lext; match = 257; break;
315 -- case DISTS: base = dbase; extra = dext; }
316 let mut base : Array UInt16 := #[] -- NULL
317 let mut extra : Array UInt16 := #[] -- NULL
318 let mut match_ : UInt32 := 0
319 if type == CODES then
320 match_ := 20
321 else if type == LENS then
322 base := lbase; extra := lext; match_ := 257
323 else if type == DISTS then
324 base := dbase; extra := dext
325 -- huff = 0; sym = 0; len = min; next = *table; curr = root; drop = 0; low = (unsigned)(-1);
326 -- used = 1U << root; mask = used - 1;
327 let used ← shl32 1 root
328 let s : TS := { huff := 0, sym := 0, len := min, curr := root, drop := 0, low := 0xffffffff, used,
329 min := min, fill := 0, incr := 0, mask := used - 1, left, next := table, here := default,
330 count, exit := 0 }
331 -- if ((type == LENS && used > ENOUGH_LENS) || (type == DISTS && used > ENOUGH_DISTS)) return 1;
332 if tooBig type used then return (1, table, bits)
333 -- for (;;) { ... }
334 let c : Ctx := { type, lens, work, table, root, max, base, extra, match_ }
335 let s ← cwhile (fun s => pure (s.exit == 0, s)) (buildStep c) s
336 -- (return 1 from inside the loop)
337 if s.exit == 2 then return (1, table, bits)
338 let mut s := s
339 -- if (huff != 0) {
340 if s.huff != 0 then
341 -- here.op = (unsigned char)64; here.bits = (unsigned char)(len - drop); here.val = (unsigned short)0;
342 s := { s with here := ⟨64, (s.len - s.drop).toUInt8, 0⟩ }
343 -- next[huff] = here;
344 storeCode s.next s.huff.toNat s.here
345 -- *table += used; *bits = root; return 0;
346 let table ← table.add s.used.toNat
347 return (0, table, root)
348
349/-- `void inflate_fixed(struct inflate_state FAR *state)` -/
350def inflate_fixed (state : InflateStatePtr) : M Unit := do
351 -- state->lencode = lenfix;
352 let st ← ldInflateState state
353 stInflateState state { st with lencode := .ref .st_lenfix 0 }
354 -- state->lenbits = 9;
355 let st ← ldInflateState state
356 stInflateState state { st with lenbits := 9 }
357 -- state->distcode = distfix;
358 let st ← ldInflateState state
359 stInflateState state { st with distcode := .ref .st_distfix 0 }
360 -- state->distbits = 5;
361 let st ← ldInflateState state
362 stInflateState state { st with distbits := 5 }
363
364end Zlib.Inftrees