uncompr.c.lean

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»
2import ZlibF.Zlib.«inflate.c»
3
4/-!
5# uncompr.c — faithful translation
6
7Source: `uncompr.c` of the verified source, default x86_64 Linux build.
8
9Decisions (see `docs/design/external-io.md`):
10* `z_stream stream;` is a local record made by `allocLocalZ` (no allocation oracle: automatic storage cannot fail),
11  with arbitrary content, and freed before every return.
12* `(Bytef *)&stream.reserved` (D-5) is a local 8-byte block, freed before every return. It is only ever passed as
13  `next_out` with `avail_out == 0`.
14* A pointer to a scalar (`z_size_t *destLen`, `uLong *sourceLen`) is a pointer to an 8-byte block holding the
15  value in little-endian order (`load64`/`store64` of `gzguts.h.lean`).
16* `inflateInit(&stream)` is `inflateInit_(&stream, ZLIB_VERSION, (int)sizeof(z_stream))`, `sizeof(z_stream) == 112`.
17-/
18
19namespace Zlib.Uncompr
20open C Zlib.GzFs Zlib.Gzguts
21open Zlib.Inflate (inflateInit_ inflate inflateEnd)
22
23/-- A local `z_stream`: a fresh record with arbitrary integers and null pointers, outside the allocation oracle
24(automatic storage cannot fail). Made by the runtime allocator `allocZStream` with the oracle set to succeed. -/
25def allocLocalZ : M ZStreamPtr := fun h =>
26  match allocZStream { h with allocOk := fun _ => true } with
27  | .ok (p, h') => .ok (p, { h' with allocOk := h.allocOk, nalloc := h.nalloc })
28  | .error e => .error e
29
30structure UncLoop where
31  err : Int32
32  len : UInt64
33  left : UInt64
34
35/-- `int ZEXPORT uncompress2_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t *sourceLen)` -/
36def uncompress2_z (dest : BPtr) (destLen : BPtr) (source : BPtr) (sourceLen : BPtr) : M Int32 := do
37  -- z_stream stream; int err; const uInt max = (uInt)-1; z_size_t len, left;
38  let stream ← allocLocalZ
39  let reserved ← allocLocal 8
40  let max : UInt32 := 0xFFFFFFFF
41  let free : M Unit := do
42    freeB reserved
43    freeZStream stream
44  -- if (sourceLen == Z_NULL || (*sourceLen > 0 && source == Z_NULL) || destLen == Z_NULL || (*destLen > 0 && dest == Z_NULL))
45  --   return Z_STREAM_ERROR;
46  let mut bad := false
47  if sourceLen == .null then bad := true
48  else if (← load64 sourceLen) > 0 && source == .null then bad := true
49  else if destLen == .null then bad := true
50  else if (← load64 destLen) > 0 && dest == .null then bad := true
51  if bad then
52    free
53    return Z_STREAM_ERROR
54  -- len = *sourceLen; left = *destLen;
55  let len ← load64 sourceLen
56  let left ← load64 destLen
57  -- if (left == 0 && dest == Z_NULL) dest = (Bytef *)&stream.reserved;
58  let dest := if left == 0 && dest == .null then reserved else dest
59  -- stream.next_in = (z_const Bytef *)source; stream.avail_in = 0; zalloc, zfree, opaque = 0;
60  updZ stream fun z => { z with next_in := source, avail_in := 0, zalloc := .null, zfree := .null, «opaque» := .null }
61  -- err = inflateInit(&stream); if (err != Z_OK) return err;
62  let ver ← Zlib.GzFs.strLit ZLIB_VERSION
63  let err ← inflateInit_ stream ver 112
64  if err != Z_OK then
65    free
66    return err
67  -- stream.next_out = dest; stream.avail_out = 0;
68  updZ stream fun z => { z with next_out := dest, avail_out := 0 }
69  -- do { ... } while (err == Z_OK);
70  let l ← cdoWhile
71    (fun (l : UncLoop) => do
72      let mut l := l
73      -- if (stream.avail_out == 0) { stream.avail_out = left > (z_size_t)max ? max : (uInt)left; left -= stream.avail_out; }
74      if (← ldZ stream).avail_out == 0 then
75        let a : UInt32 := if l.left > max.toUInt64 then max else l.left.toUInt32
76        updZ stream fun z => { z with avail_out := a }
77        l := { l with left := l.left - a.toUInt64 }
78      -- if (stream.avail_in == 0) { stream.avail_in = len > (z_size_t)max ? max : (uInt)len; len -= stream.avail_in; }
79      if (← ldZ stream).avail_in == 0 then
80        let a : UInt32 := if l.len > max.toUInt64 then max else l.len.toUInt32
81        updZ stream fun z => { z with avail_in := a }
82        l := { l with len := l.len - a.toUInt64 }
83      -- err = inflate(&stream, Z_NO_FLUSH);
84      let err ← inflate stream Z_NO_FLUSH
85      return { l with err })
86    (fun l => pure (l.err == Z_OK, l))
87    { err, len, left }
88  -- len += stream.avail_in; left += stream.avail_out; *sourceLen -= len; *destLen -= left;
89  let z ← ldZ stream
90  let len := l.len + z.avail_in.toUInt64
91  let left := l.left + z.avail_out.toUInt64
92  store64 sourceLen ((← load64 sourceLen) - len)
93  store64 destLen ((← load64 destLen) - left)
94  -- inflateEnd(&stream);
95  let _ ← inflateEnd stream
96  -- return err == Z_STREAM_END ? Z_OK : err == Z_NEED_DICT ? Z_DATA_ERROR : err == Z_BUF_ERROR && len == 0 ? Z_DATA_ERROR : err;
97  let err := l.err
98  let r : Int32 :=
99    if err == Z_STREAM_END then Z_OK
100    else if err == Z_NEED_DICT then Z_DATA_ERROR
101    else if err == Z_BUF_ERROR && len == 0 then Z_DATA_ERROR
102    else err
103  free
104  return r
105
106/-- `int ZEXPORT uncompress2(Bytef *dest, uLongf *destLen, const Bytef *source, uLong *sourceLen)` -/
107def uncompress2 (dest : BPtr) (destLen : BPtr) (source : BPtr) (sourceLen : BPtr) : M Int32 := do
108  -- int ret; z_size_t got = *destLen, used = *sourceLen;
109  let got ← allocLocal 8
110  let used ← allocLocal 8
111  store64 got (← load64 destLen)
112  store64 used (← load64 sourceLen)
113  -- ret = uncompress2_z(dest, &got, source, &used);
114  let ret ← uncompress2_z dest got source used
115  -- *sourceLen = (uLong)used; *destLen = (uLong)got;
116  store64 sourceLen (← load64 used)
117  store64 destLen (← load64 got)
118  freeB got
119  freeB used
120  return ret
121
122/-- `int ZEXPORT uncompress_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t sourceLen)` -/
123def uncompress_z (dest : BPtr) (destLen : BPtr) (source : BPtr) (sourceLen : UInt64) : M Int32 := do
124  -- z_size_t used = sourceLen;
125  let used ← allocLocal 8
126  store64 used sourceLen
127  let r ← uncompress2_z dest destLen source used
128  freeB used
129  return r
130
131/-- `int ZEXPORT uncompress(Bytef *dest, uLongf *destLen, const Bytef *source, uLong sourceLen)` -/
132def uncompress (dest : BPtr) (destLen : BPtr) (source : BPtr) (sourceLen : UInt64) : M Int32 := do
133  -- uLong used = sourceLen;
134  let used ← allocLocal 8
135  store64 used sourceLen
136  let r ← uncompress2 dest destLen source used
137  freeB used
138  return r
139
140end Zlib.Uncompr