REFERENCE / ZLIB × LEAN
inffast.c.lean
Source snapshot ·
b94e4b80cdf351fe · 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.«zutil.c»
4
5/-!
6# inffast.c — faithful translation
7
8Source: `inffast.c`, default x86_64 Linux build (LP64). `ASMINF`, `INFLATE_STRICT` and
9`INFLATE_ALLOW_INVALID_DISTANCE_TOOFAR_ARRR` are undefined: the C `inflate_fast` is live, the `dmax` test and the
10`ARRR` block (with its two `continue`s) are dead and omitted. `Tracevv` expands to nothing.
11
12Mapping of the control flow (decision, per `docs/design/translation.md`):
13
14* `do { ... } while (in < last && out < end);` is `cdoWhile`; every `break` of the C leaves that loop *without*
15 evaluating its condition, so the locals carry a flag `broke` and the condition is `false` when it is set.
16* The labels `dolen` and `dodist` are the entry points of two blocks; `goto dolen` / `goto dodist` re-enter the same
17 block. Each block is a `do ... while (again)` loop (`cdoWhile`) whose flag (`againL`, `againD`) is set by the
18 `goto`; the block clears its flag first. The `dodist` block sits inside the length branch of the `dolen` block
19 exactly where the C text has it.
20* All locals live in one record `L` (the loop-carried state of the whole function body).
21
22Decisions on the model: `unsigned long` shifts and `unsigned` shifts fault for a count at or above the width (a C
23undefined behaviour that the entry assumptions exclude); `in`, `out`, `from`, `last`, `end`, `beg` are `BPtr`s and
24every addition, subtraction, difference and comparison of them is checked by the runtime; the error strings are
25literals made by `Zlib.Zutil.strLit`; `strm->state` is cast to an inflate state (a fault for a deflate state).
26-/
27
28namespace Zlib.Inffast
29open C
30
31/-! ### Small checked operations -/
32
33/-- `x << n` for `unsigned`: undefined if `n >= 32`. -/
34def shl32 (x n : UInt32) : M UInt32 :=
35 if n < 32 then pure (x <<< n) else ub "shift count out of range"
36
37/-- `x << n` for `unsigned long`: undefined if `n >= 64`. -/
38def shl64 (x n : UInt64) : M UInt64 :=
39 if n < 64 then pure (x <<< n) else ub "shift count out of range"
40
41/-- `x >> n` for `unsigned long`: undefined if `n >= 64`. -/
42def shr64 (x n : UInt64) : M UInt64 :=
43 if n < 64 then pure (x >>> n) else ub "shift count out of range"
44
45/-- A `long` result: a fault if it does not fit. -/
46def chk64 (v : Int) : M Int64 :=
47 if -9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807 then pure (Int64.ofInt v) else ub "signed integer overflow"
48
49/-- `p - n` for a pointer and an `unsigned` count. -/
50def subn (p : BPtr) (n : UInt32) : M BPtr := p.add (-(n.toNat : Int))
51
52/-! ### The locals -/
53
54/-- The local variables of `inflate_fast` that change during the loop. -/
55structure L where
56 in_ : BPtr
57 out : BPtr
58 hold : UInt64
59 bits : UInt32
60 here : CodePtr
61 op : UInt32
62 len : UInt32
63 dist : UInt32
64 from_ : BPtr
65 broke : Bool
66 againL : Bool
67 againD : Bool
68
69/-- What `inflate_fast` reads once and does not change. -/
70structure Ctx where
71 strm : ZStreamPtr
72 state : InflateStatePtr
73 last : BPtr
74 beg : BPtr
75 end_ : BPtr
76 wsize : UInt32
77 whave : UInt32
78 wnext : UInt32
79 window : BPtr
80 lcode : CodePtr
81 dcode : CodePtr
82 lmask : UInt32
83 dmask : UInt32
84
85/-- `hold += (unsigned long)(*in++) << bits; bits += 8;` -/
86def pull (l : L) : M L := do
87 let b ← load8 l.in_
88 let in_ ← l.in_.add 1
89 let sh ← shl64 b.toUInt64 l.bits.toUInt64
90 pure { l with in_, hold := l.hold + sh, bits := l.bits + 8 }
91
92/-- `*out++ = *from++;` -/
93def copy1 (l : L) : M L := do
94 let b ← load8 l.from_
95 let from_ ← l.from_.add 1
96 store8 l.out b
97 let out ← l.out.add 1
98 pure { l with from_, out }
99
100/-- `do { *out++ = *from++; } while (--op);` -/
101def copyOp (l : L) : M L :=
102 cdoWhile copy1 (fun l => let op := l.op - 1; pure (op != 0, { l with op })) l
103
104/-- `strm->msg = (z_const char *)"..."; state->mode = BAD;` -/
105def badData (c : Ctx) (msg : String) : M Unit := do
106 let p ← Zlib.Zutil.strLit msg
107 let st ← ldZStream c.strm
108 stZStream c.strm { st with msg := p }
109 let s ← ldInflateState c.state
110 stInflateState c.state { s with mode := BAD }
111
112/-- The tail of the distance block, from the test `if (dist > op)`: copy the match. `dist` and `len` are set;
113`op = out - beg`. -/
114def copyMatch (c : Ctx) (l : L) : M L := do
115 let mut l := l
116 -- if (dist > op) { /* see if copy from window */
117 if l.dist > l.op then
118 -- op = dist - op; /* distance back in window */
119 l := { l with op := l.dist - l.op }
120 -- if (op > whave) {
121 if l.op > c.whave then
122 -- if (state->sane) { strm->msg = "invalid distance too far back"; state->mode = BAD; break; }
123 let s ← ldInflateState c.state
124 if s.sane != 0 then
125 badData c "invalid distance too far back"
126 return { l with broke := true }
127 -- (INFLATE_ALLOW_INVALID_DISTANCE_TOOFAR_ARRR is not defined)
128 -- from = window;
129 l := { l with from_ := c.window }
130 -- if (wnext == 0) { /* very common case */
131 if c.wnext == 0 then
132 -- from += wsize - op;
133 l := { l with from_ := ← l.from_.add (c.wsize - l.op).toNat }
134 -- if (op < len) { /* some from window */
135 if l.op < l.len then
136 -- len -= op; do { *out++ = *from++; } while (--op); from = out - dist;
137 l := { l with len := l.len - l.op }
138 l ← copyOp l
139 l := { l with from_ := ← subn l.out l.dist }
140 -- else if (wnext < op) { /* wrap around window */
141 else if c.wnext < l.op then
142 -- from += wsize + wnext - op;
143 l := { l with from_ := ← l.from_.add (c.wsize + c.wnext - l.op).toNat }
144 -- op -= wnext;
145 l := { l with op := l.op - c.wnext }
146 -- if (op < len) { /* some from end of window */
147 if l.op < l.len then
148 -- len -= op; do { *out++ = *from++; } while (--op); from = window;
149 l := { l with len := l.len - l.op }
150 l ← copyOp l
151 l := { l with from_ := c.window }
152 -- if (wnext < len) { /* some from start of window */
153 if c.wnext < l.len then
154 -- op = wnext; len -= op; do { *out++ = *from++; } while (--op); from = out - dist;
155 l := { l with op := c.wnext }
156 l := { l with len := l.len - l.op }
157 l ← copyOp l
158 l := { l with from_ := ← subn l.out l.dist }
159 -- else { /* contiguous in window */
160 else
161 -- from += wnext - op;
162 l := { l with from_ := ← l.from_.add (c.wnext - l.op).toNat }
163 -- if (op < len) { /* some from window */
164 if l.op < l.len then
165 -- len -= op; do { *out++ = *from++; } while (--op); from = out - dist;
166 l := { l with len := l.len - l.op }
167 l ← copyOp l
168 l := { l with from_ := ← subn l.out l.dist }
169 -- while (len > 2) { *out++ = *from++; *out++ = *from++; *out++ = *from++; len -= 3; }
170 l ← cwhile (fun l => pure (l.len > 2, l))
171 (fun l => do
172 let l ← copy1 l
173 let l ← copy1 l
174 let l ← copy1 l
175 pure { l with len := l.len - 3 }) l
176 -- if (len) { *out++ = *from++; if (len > 1) *out++ = *from++; }
177 if l.len != 0 then
178 l ← copy1 l
179 if l.len > 1 then l ← copy1 l
180 -- else {
181 else
182 -- from = out - dist; /* copy direct from output */
183 l := { l with from_ := ← subn l.out l.dist }
184 -- do { *out++ = *from++; *out++ = *from++; *out++ = *from++; len -= 3; } while (len > 2);
185 l ← cdoWhile
186 (fun l => do
187 let l ← copy1 l
188 let l ← copy1 l
189 let l ← copy1 l
190 pure { l with len := l.len - 3 })
191 (fun l => pure (l.len > 2, l)) l
192 -- if (len) { *out++ = *from++; if (len > 1) *out++ = *from++; }
193 if l.len != 0 then
194 l ← copy1 l
195 if l.len > 1 then l ← copy1 l
196 pure l
197
198/-- The block that starts at the label `dodist:`. Sets `againD` for `goto dodist`, `broke` for `break`. -/
199def dodist (c : Ctx) (l : L) : M L := do
200 let mut l := { l with againD := false }
201 -- op = (unsigned)(here->bits);
202 let e ← l.here.load
203 l := { l with op := e.bits.toUInt32 }
204 -- hold >>= op; bits -= op;
205 l := { l with hold := ← shr64 l.hold l.op.toUInt64 }
206 l := { l with bits := l.bits - l.op }
207 -- op = (unsigned)(here->op);
208 let e ← l.here.load
209 l := { l with op := e.op.toUInt32 }
210 -- if (op & 16) { /* distance base */
211 if l.op &&& 16 != 0 then
212 -- dist = (unsigned)(here->val);
213 let e ← l.here.load
214 l := { l with dist := e.val.toUInt32 }
215 -- op &= 15; /* number of extra bits */
216 l := { l with op := l.op &&& 15 }
217 -- if (bits < op) { hold += ... ; bits += 8; if (bits < op) { hold += ...; bits += 8; } }
218 if l.bits < l.op then
219 l ← pull l
220 if l.bits < l.op then
221 l ← pull l
222 -- dist += (unsigned)hold & ((1U << op) - 1);
223 let m ← shl32 1 l.op
224 l := { l with dist := l.dist + (l.hold.toUInt32 &&& (m - 1)) }
225 -- (INFLATE_STRICT is not defined)
226 -- hold >>= op; bits -= op;
227 l := { l with hold := ← shr64 l.hold l.op.toUInt64 }
228 l := { l with bits := l.bits - l.op }
229 -- op = (unsigned)(out - beg); /* max distance in output */
230 let d ← l.out.diff c.beg
231 l := { l with op := d.toUInt64.toUInt32 }
232 copyMatch c l
233 -- else if ((op & 64) == 0) { /* 2nd level distance code */
234 else if l.op &&& 64 == 0 then
235 -- here = dcode + here->val + (hold & ((1U << op) - 1));
236 let e ← l.here.load
237 let h1 ← c.dcode.add e.val.toNat
238 let m ← shl32 1 l.op
239 let here ← h1.add (l.hold &&& (m - 1).toUInt64).toNat
240 -- goto dodist;
241 pure { l with here, againD := true }
242 else
243 -- strm->msg = "invalid distance code"; state->mode = BAD; break;
244 badData c "invalid distance code"
245 pure { l with broke := true }
246
247/-- The block that starts at the label `dolen:`. Sets `againL` for `goto dolen`, `broke` for `break`. -/
248def dolen (c : Ctx) (l : L) : M L := do
249 let mut l := { l with againL := false }
250 -- op = (unsigned)(here->bits);
251 let e ← l.here.load
252 l := { l with op := e.bits.toUInt32 }
253 -- hold >>= op; bits -= op;
254 l := { l with hold := ← shr64 l.hold l.op.toUInt64 }
255 l := { l with bits := l.bits - l.op }
256 -- op = (unsigned)(here->op);
257 let e ← l.here.load
258 l := { l with op := e.op.toUInt32 }
259 -- if (op == 0) { /* literal */
260 if l.op == 0 then
261 -- *out++ = (unsigned char)(here->val);
262 let e ← l.here.load
263 store8 l.out e.val.toUInt8
264 pure { l with out := ← l.out.add 1 }
265 -- else if (op & 16) { /* length base */
266 else if l.op &&& 16 != 0 then
267 -- len = (unsigned)(here->val);
268 let e ← l.here.load
269 l := { l with len := e.val.toUInt32 }
270 -- op &= 15; /* number of extra bits */
271 l := { l with op := l.op &&& 15 }
272 -- if (op) {
273 if l.op != 0 then
274 -- if (bits < op) { hold += (unsigned long)(*in++) << bits; bits += 8; }
275 if l.bits < l.op then l ← pull l
276 -- len += (unsigned)hold & ((1U << op) - 1);
277 let m ← shl32 1 l.op
278 l := { l with len := l.len + (l.hold.toUInt32 &&& (m - 1)) }
279 -- hold >>= op; bits -= op;
280 l := { l with hold := ← shr64 l.hold l.op.toUInt64 }
281 l := { l with bits := l.bits - l.op }
282 -- if (bits < 15) { two pulls }
283 if l.bits < 15 then
284 l ← pull l
285 l ← pull l
286 -- here = dcode + (hold & dmask);
287 l := { l with here := ← c.dcode.add (l.hold &&& c.dmask.toUInt64).toNat }
288 -- dodist: ...
289 cdoWhile (dodist c) (fun l => pure (l.againD, l)) l
290 -- else if ((op & 64) == 0) { /* 2nd level length code */
291 else if l.op &&& 64 == 0 then
292 -- here = lcode + here->val + (hold & ((1U << op) - 1));
293 let e ← l.here.load
294 let h1 ← c.lcode.add e.val.toNat
295 let m ← shl32 1 l.op
296 let here ← h1.add (l.hold &&& (m - 1).toUInt64).toNat
297 -- goto dolen;
298 pure { l with here, againL := true }
299 -- else if (op & 32) { /* end-of-block */
300 else if l.op &&& 32 != 0 then
301 -- state->mode = TYPE; break;
302 let s ← ldInflateState c.state
303 stInflateState c.state { s with mode := TYPE }
304 pure { l with broke := true }
305 else
306 -- strm->msg = "invalid literal/length code"; state->mode = BAD; break;
307 badData c "invalid literal/length code"
308 pure { l with broke := true }
309
310/-- One pass of the body of the `do ... while` loop of `inflate_fast`. -/
311def inflate_fast_body (c : Ctx) (l : L) : M L := do
312 let mut l := l
313 -- if (bits < 15) { hold += (unsigned long)(*in++) << bits; bits += 8; (twice) }
314 if l.bits < 15 then
315 l ← pull l
316 l ← pull l
317 -- here = lcode + (hold & lmask);
318 l := { l with here := ← c.lcode.add (l.hold &&& c.lmask.toUInt64).toNat }
319 -- dolen: ...
320 cdoWhile (dolen c) (fun l => pure (l.againL, l)) l
321
322/-- `void ZLIB_INTERNAL inflate_fast(z_streamp strm, unsigned start)` -/
323def inflate_fast (strm : ZStreamPtr) (start : UInt32) : M Unit := do
324 -- state = (struct inflate_state FAR *)strm->state;
325 let sm ← ldZStream strm
326 let state ← castInflateState sm.state
327 -- in = strm->next_in;
328 let in_ := sm.next_in
329 -- last = in + (strm->avail_in - 5);
330 let last ← in_.add (sm.avail_in - 5).toNat
331 -- out = strm->next_out;
332 let out := sm.next_out
333 -- beg = out - (start - strm->avail_out);
334 let beg ← subn out (start - sm.avail_out)
335 -- end = out + (strm->avail_out - 257);
336 let end_ ← out.add (sm.avail_out - 257).toNat
337 -- wsize = state->wsize; whave = state->whave; wnext = state->wnext; window = state->window;
338 -- hold = state->hold; bits = state->bits; lcode = state->lencode; dcode = state->distcode;
339 let s ← ldInflateState state
340 -- lmask = (1U << state->lenbits) - 1;
341 let lmask := (← shl32 1 s.lenbits) - 1
342 -- dmask = (1U << state->distbits) - 1;
343 let dmask := (← shl32 1 s.distbits) - 1
344 let c : Ctx := { strm, state, last, beg, end_, wsize := s.wsize, whave := s.whave, wnext := s.wnext,
345 window := s.window, lcode := s.lencode, dcode := s.distcode, lmask, dmask }
346 let l : L := { in_, out, hold := s.hold, bits := s.bits, here := default, op := 0, len := 0, dist := 0,
347 from_ := default, broke := false, againL := false, againD := false }
348 -- do { ... } while (in < last && out < end);
349 let l ← cdoWhile (inflate_fast_body c)
350 (fun l => do
351 -- a `break` leaves the loop without evaluating the condition
352 if l.broke then pure (false, l)
353 else if ← Ptr.lt l.in_ c.last then pure (← Ptr.lt l.out c.end_, l)
354 else pure (false, l)) l
355 -- len = bits >> 3;
356 let len := l.bits >>> 3
357 -- in -= len;
358 let in_ ← subn l.in_ len
359 -- bits -= len << 3;
360 let bits := l.bits - (len <<< 3)
361 -- hold &= (1U << bits) - 1;
362 let hold := l.hold &&& ((← shl32 1 bits) - 1).toUInt64
363 -- strm->next_in = in; strm->next_out = out;
364 -- strm->avail_in = (unsigned)(in < last ? 5 + (last - in) : 5 - (in - last));
365 let ai : Int64 ←
366 if ← Ptr.lt in_ last then do let d ← last.diff in_; chk64 (5 + d.toInt)
367 else do let d ← in_.diff last; chk64 (5 - d.toInt)
368 -- strm->avail_out = (unsigned)(out < end ? 257 + (end - out) : 257 - (out - end));
369 let ao : Int64 ←
370 if ← Ptr.lt l.out end_ then do let d ← end_.diff l.out; chk64 (257 + d.toInt)
371 else do let d ← l.out.diff end_; chk64 (257 - d.toInt)
372 let sm ← ldZStream strm
373 stZStream strm { sm with next_in := in_, next_out := l.out, avail_in := ai.toUInt64.toUInt32,
374 avail_out := ao.toUInt64.toUInt32 }
375 -- state->hold = hold; state->bits = bits;
376 let s ← ldInflateState state
377 stInflateState state { s with hold, bits }
378
379end Zlib.Inffast