inflateMark
查询当前码位置,用于索引。
完整章节与共同规则 ↗ecafc184cdf44b7f · 对应提交的原文 ↗先看本函数的前置条件和返回结果;可展开下方共同规则,查看整组接口的缓冲区与所有权要求。
long ZEXPORT inflateMark(z_streamp strm);
查询当前码位置,用于索引。
返回的一个整数打包了两种进度。back 按比特计,描述从当前位位置回到本次编码起点的距离;progress 按字节计,描述存储块尚未复制的量或当前匹配已经输出的量。下面的乘数 65536 即 2^16,用于把两部分放进同一个结果,不表示窗口大小。
定义域 受限定义域:任意模式的有效流。
内存与状态效果 只读查询。
前置条件 满足公共有效流条件。
返回与保证 返回 back * 65536 + progress:back 是向后回到当前码所需的位数;在码之间/头部内/存储块内为 -1。progress 为剩余存储块字节数、已输出匹配字节数,其他情况为零。不改变任何内容,不分配/释放。
边界情况 流检查失败返回 -65536。该值也可能出现在有效流上,因此不能单凭它识别错误。
本组共同前提与范围
使用 inflate 流分批解码输入,同时控制输出空间。初始化时选择 zlib、gzip 或不带封装的 raw DEFLATE,随后提供更多输入或空间继续,直到完成、请求字典或发生错误。无论出现哪种结果,inflateEnd 都可释放解码器。整块缓冲区的 zlib 解码见 uncompress。
| 任务 | 条目 |
|---|---|
| 开始或复用 | 初始化、配置初始化、重置、新配置、保留历史 |
| 解码或提供元数据 | 解压、设置字典、读取历史、gzip 头 |
| 恢复或检查 | 同步搜索、同步点、位置标记、表使用量 |
| 调整或分支 | 预置位、校验、距离选项、复制 |
| 释放存储 | 结束 |
聚焦契约遵循固定版本的 inflate.c 和 zlib.h,采用默认 LP64 Linux 构建,启用 gzip,不启用可选的无效距离或严格距离模式。范围更广的已登记公开目标保持各自定义域。术语见契约约定,证明状态和剩余工作见进度。
公共条件
调用者与解码器各自保留不同的内容。调用者提供本轮输入和输出缓冲区;解码器保留当前解析阶段、尚未用完的位,以及可能供后续复制使用的历史。更换调用者的输出数组,并不会开始一个新解码任务。
next_in 是本轮未读输入的起点,avail_in 是可读字节数;next_out 是下一个输出位置,avail_out 是从这里开始的剩余可写字节数。例如一块 5 字节输出数组返回时剩余 2 字节空间,就说明本轮写入了 3 字节。先接走这些结果,再把指针和容量设置为下一块可写区域。
下列所有契约都有受限定义域。仅凭 C 指针类型,不能提供这里要求的存储、生命周期或调用历史。
- 有效流已成功初始化或复制,尚未结束,保留库拥有的状态,且不发生并发调用。使用默认分配器和释放函数。初始化调用接收可写、尚未有效初始化为流的对象,分配器字段为 NULL 或默认函数。
- 可读或可写范围在整个调用期间都具有所述容量。调用者范围与流及流拥有的存储分离。输入与输出范围不重叠。字典目标、已登记头部记录及其目标缓冲区彼此分离,也与流分离。使用已登记头部存储的调用还要求它与输入/输出范围分离。这些是聚焦定义域的显式限制。
- 调用者拥有流对象及缓冲区。库拥有状态和可选窗口。调用只改变自己的流、拥有的存储、所述输出范围和任何已登记头部目标。它绝不释放调用者缓冲区。
- 流检查拒绝时返回
Z_STREAM_ERROR,不发生变化,除非查询或复制契约另有说明。这覆盖 NULL 和可安全读取但未通过检查的记录,不覆盖悬空或任意指针。检查要求分配器、状态、状态的回指针和有效模式满足条件。 - 计数器使用 C 无符号位宽并回绕。没有契约假设分配成功。解码、字典或分配错误之后,仍可调用
inflateEnd。
flowchart LR
I["初始化"] --> F["inflate"]
F -->|"Z_NEED_DICT"| D["设置字典"] --> F
F -->|"更多空间或输入"| F
F -->|"结束或放弃"| E["结束"]
F -->|"数据错误"| R["重置或同步搜索"] --> F
形式化约定
ZlibF.Spec.Public.Goal.inflateMark
证明状态:已登记证明 · 证明记录与剩余工作
/-- `long inflateMark(z_streamp strm)`.
The high half counts code bits; the low half counts remaining stored bytes or match bytes
already copied. The internal ranges are obligations of the stream invariant. -/
def Goal.inflateMark : Prop :=
CheckedInflate Zlib.Inflate.inflateMark (-65536) <|
∀ h r i z s, InflateView h r i z s →
C.run (Zlib.Inflate.inflateMark (some r)) h = .ok
(Int64.ofInt (s.back.toInt * 65536 +
(if s.mode = COPY then s.length.toNat else
if s.mode = MATCH then (s.was - s.length).toNat else 0)), h)相关定义与源码 ↗