zutil.c.lean

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

1import ZlibF.Runtime.Alloc
2
3/-!
4# zutil.c — faithful translation
5
6Source: `zutil.c` of the verified source, default x86_64 Linux build (LP64, `Z_SOLO`, `ZLIB_DEBUG`, `SYS16BIT`,
7`_WIN32_WCE` undefined; `STDC` and `HAVE_MEMCPY` defined, so the `#ifndef HAVE_MEMCPY` functions `zmemcpy`,
8`zmemcmp`, `zmemzero` are not compiled: the macros of `zutil.h` expand to `memcpy`, `memcmp`, `memset`, which the
9runtime provides). Live: `z_errmsg`, `zlibVersion`, `zlibCompileFlags`, `zError`, `zcalloc`, `zcfree`.
10
11Decisions:
12
13* **String literals.** A string literal is a static read-only array of bytes in C. `strLit` is `strLitRef`: the pointer
14  to the literal number `i` of `strTable` (`BRef.str i`), the same pointer every time, no block allocated, nothing
15  to free. The set of literals is the string literals of the library sources; a text outside it is a fault.
16* `z_errmsg` (an array of 10 pointers to literals) is the Lean array of the 10 texts; `ERR_MSG` indexes it and then
17  gives the literal.
18* `sizeof` values of the LP64 target: `uInt` 4, `uLong` 8, `voidpf` 8, `z_off_t` 8.
19-/
20
21namespace Zlib.Zutil
22open C
23
24/-- A string literal of the C sources (see the file comment): `strLitRef s`. -/
25def strLit (s : String) : M BPtr := strLitRef s
26
27/-- `z_const char * const z_errmsg[10]`: the texts, indexed by `2 - error code`. -/
28def z_errmsg : Array String :=
29  #["need dictionary",      -- Z_NEED_DICT       2
30    "stream end",           -- Z_STREAM_END      1
31    "",                     -- Z_OK              0
32    "file error",           -- Z_ERRNO         (-1)
33    "stream error",         -- Z_STREAM_ERROR  (-2)
34    "data error",           -- Z_DATA_ERROR    (-3)
35    "insufficient memory",  -- Z_MEM_ERROR     (-4)
36    "buffer error",         -- Z_BUF_ERROR     (-5)
37    "incompatible version", -- Z_VERSION_ERROR (-6)
38    ""]
39
40/-- `const char * ZEXPORT zlibVersion(void)` -/
41def zlibVersion : M BPtr :=
42  -- return ZLIB_VERSION;
43  strLit ZLIB_VERSION
44
45/-- `uLong ZEXPORT zlibCompileFlags(void)` -/
46def zlibCompileFlags : M UInt64 := do
47  -- flags = 0;
48  let flags : UInt64 := 0
49  -- switch ((int)(sizeof(uInt))) { case 2: break; case 4: flags += 1; break; case 8: flags += 2; break; default: flags += 3; }
50  let sz : Int32 := 4
51  let flags := if sz == 2 then flags else if sz == 4 then flags + 1 else if sz == 8 then flags + 2 else flags + 3
52  -- switch ((int)(sizeof(uLong))) { ... case 4: flags += 1 << 2; case 8: flags += 2 << 2; default: flags += 3 << 2; }
53  let sz : Int32 := 8
54  let flags := if sz == 2 then flags else if sz == 4 then flags + ((1 : UInt64) <<< 2) else if sz == 8 then flags + ((2 : UInt64) <<< 2)
55    else flags + ((3 : UInt64) <<< 2)
56  -- switch ((int)(sizeof(voidpf))) { ... << 4 }
57  let sz : Int32 := 8
58  let flags := if sz == 2 then flags else if sz == 4 then flags + ((1 : UInt64) <<< 4) else if sz == 8 then flags + ((2 : UInt64) <<< 4)
59    else flags + ((3 : UInt64) <<< 4)
60  -- switch ((int)(sizeof(z_off_t))) { ... << 6 }
61  let sz : Int32 := 8
62  let flags := if sz == 2 then flags else if sz == 4 then flags + ((1 : UInt64) <<< 6) else if sz == 8 then flags + ((2 : UInt64) <<< 6)
63    else flags + ((3 : UInt64) <<< 6)
64  -- ZLIB_DEBUG, ZLIB_WINAPI, BUILDFIXED, DYNAMIC_CRC_TABLE, NO_GZCOMPRESS, NO_GZIP, PKZIP_BUG_WORKAROUND, FASTEST,
65  -- NO_vsnprintf, HAS_vsnprintf_void: all undefined in the default build (STDC is defined, so the
66  -- `#else flags += 1L << 24` branch is dead).
67  -- return flags;
68  return flags
69
70/-- `const char * ZEXPORT zError(int err)`  (`ERR_MSG(err)` is
71`z_errmsg[(err) < -6 || (err) > 2 ? 9 : 2 - (err)]`) -/
72def zError (err : Int32) : M BPtr := do
73  let i : Int32 := if err < -6 || err > 2 then 9 else 2 - err
74  -- the index is in 0..9 for every err, so the access is inside the array
75  match z_errmsg[i.toInt.toNat]? with
76  | some s => strLit s
77  | none => ub "z_errmsg index outside its array"
78
79/-- `voidpf ZLIB_INTERNAL zcalloc(voidpf opaque, unsigned items, unsigned size)` (the default allocator, `malloc` branch
80since `sizeof(uInt) > 2`; the product is computed in `unsigned`). -/
81def zcalloc («opaque» : BPtr) (items size : UInt32) : M BPtr := do
82  -- (void)opaque;
83  let _ := «opaque»
84  -- return sizeof(uInt) > 2 ? (voidpf)malloc(items * size) : (voidpf)calloc(items, size);
85  allocB (items * size).toNat
86
87/-- `void ZLIB_INTERNAL zcfree(voidpf opaque, voidpf ptr)` -/
88def zcfree («opaque» ptr : BPtr) : M Unit := do
89  -- (void)opaque;
90  let _ := «opaque»
91  -- free(ptr);
92  freeB ptr
93
94end Zlib.Zutil