inftrees.c.lean

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

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