inffast.c.lean

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

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