跳到正文
参考文档 / ZLIB × LEAN

6. 选择应用接口

此页源文件快照 · 6d7457983c08864e · 对应提交的原文 ↗

解码八个字节、把大型归档的解压内容复制到目标区、读取 gzip 文件末尾附近的一行, 它们共享字节含义,但使用不同的数据传递与资源协议。 这些接口的完整执行证明未完成,仍需连接实际字节传递、回调/系统调用和资源清理; 共用组合规则适用于每种接口。

目录

6.1 一次缓冲区操作包含一段流生命周期

compress 接受完整输入及目标容量,在内部管理普通压缩器。 uncompress 则管理普通解码器。两者均使用 zlib 格式,不能选择 gzip/raw。

sequenceDiagram
    participant A as 应用
    participant U as 缓冲区工具接口
    participant E as 普通流引擎
    A->>U: 输入字节、目标容量
    U->>E: 初始化
    alt 初始化成功
        loop 引擎返回 Z_OK 时继续
            U->>E: 提供可用片段并处理
            E-->>U: 更新后的游标、结果
        end
        U->>E: 结束并释放,包括处理失败的情况
        U-->>A: 已用目标长度、映射后的结果
    else 初始化失败
        U-->>A: 初始化错误
    end

接口的总长度可能比内层流字段能表示的单次字节数更大。例如,完整输入的总长度用较宽整数保存,而内层 avail_in 只计本次可提供的部分。因此,较宽的长度会切成适合引擎可用量字段的片段。 接口隐藏了流式使用规则,但其证明仍须核算游标并保证清理。

八字节示例。 对 ABABABAB,设压缩产生 m 个字节。 头尾和块描述可能使 m 大于八。默认公式给出 compressBound(8) = 21; 要证明容量足够,还必须把这个数与实际输出长度联系起来。 不同配置可能产生不同的压缩字节和 m。

解压则需要另行界定原始长度;仅凭压缩长度无法得到目标容量。 若有效流表示八个字节,而目标只有四字节,即使因缓冲区不足而失败,也必须限制在这四字节内。 此时输出区可能已经改变。

工具接口把引擎完成结果 Z_STREAM_END 映射为 Z_OK。 uncompress2 报告已消费输入和输出长度,并把字典请求及部分输入不完整的情况映射为 Z_DATA_ERROR。 契约给出精确结果及标量存储要求; 证明指南涵盖局部状态、类型转换和界限。

6.2 回调让解码器主动请求输入

inflateBack 在一次调用中主动调用输入与输出函数。 它在 infback.c 中有独立的 raw DEFLATE 实现,不是普通 inflate 的封装。

sequenceDiagram
    participant A as 应用
    participant B as 回调解码器
    participant I as 输入回调
    participant O as 输出回调
    A->>B: inflateBackInit,使用调用者拥有的窗口
    A->>B: inflateBack,提供回调
    loop 直到一个 raw 流结束或发生失败
        B->>I: 请求下一个可读输入片段
        I-->>B: 指针与计数,零表示没有输入
        Note over B: 解码到窗口,保留历史
        B->>O: 读取窗口中已产生的片段
        O-->>B: 零表示成功,非零表示失败
    end
    B-->>A: 完成或错误,以及未读输入后缀
    A->>B: inflateBackEnd 释放内部状态
    Note over A: 调用者现在可以释放窗口

图中假定初始化成功,展示一种可能的循环,不表示每次输入调用都对应一次输出调用。 初始输入可能推迟首次回调。每个输出块至多为一个窗口,结束时还可能交付非空的部分块。 窗口还用于保留历史,因此回调不得覆盖或释放它。 回调返回前必须读完或复制该片段,之后解码器可以复用这块存储。

复制到目标区。 输入回调提供归档片段,输出回调把解码后的片段复制到应用存储。 安全性要求:输入在允许替换前保持可读,窗口写入不越界,回调目标容量足够。 回调必须返回,累计提供的输入也必须有界;函数指针类型本身不保证这些条件。

输入耗尽或输出拒绝可能返回 Z_BUF_ERROR。 格式错误可能在已有输出后返回 Z_DATA_ERROR;最终输出拒绝不会覆盖已经选定的格式错误。 清理使用 inflateBackEnd。每次新的 inflateBack 调用都会开始独立的 raw 流, 不能把它当作输入暂时不足后继续原任务的调用。

回调契约说明其受限定义域; 证明指南把调用与窗口所有权联系起来。 外层若有 zlib/gzip 包装,由应用处理。

6.3 gzip 句柄把编解码器连接到文件

gzopen 创建句柄,gzread/gzwrite 传递应用字节,gzclose 释放句柄。 输入/输出操作简称 I/O,文件的实际读写由操作系统提供。缓冲区与编解码器按需初始化:打开成功不保证后续分配或 I/O 成功。 这些调用依赖明确的外部世界语义。

flowchart LR
    file["文件:压缩字节"] -->|"操作系统读取"| input["缓冲的输入"]
    input --> decoder["Gzip 解码"]
    decoder --> output["解码字节:缓冲或直接交付"]
    output -->|"gzread"| app["应用"]
    app -->|"gzwrite"| encoder["缓冲输入与 gzip 编码"]
    encoder -->|"操作系统写入"| sink["文件:压缩字节"]

读写是不同模式,缓冲使各箭头可以分别推进。 gzwrite 可能先接受字节,尚未写入文件,之后在 flush/close 时失败。 证明必须区分已接受字节、已编码字节和成功的 I/O。

gzread 在内部处理串接的 gzip 成员;普通 inflate 完成一个成员后需要调用者采取下一步操作。 普通文件读取还可能识别非 gzip 输入并原样返回。 因此其证明既包括解码,也包括透明复制。

成员分别包含 AB 和 CD。 多次读取可跨任意缓冲边界交付 ABCD, 同时保持各成员的检查与分配核算。已经返回数据后,仍可能报告后续错误。 正常到达文件结尾(EOF)、数据被截断、数据损坏和操作系统失败有不同的API 结果。 清理须覆盖按需初始化失败、部分 I/O 以及失败后的关闭;释放资源不能以最后一次写入成功为前提。 见 gzip 论证。

6.4 定位使用原始数据中的位置

gzseek(file, 100000000, SEEK_SET) 指定的是未压缩数据的第 100,000,000 字节。 gztell 给出下一次传递的逻辑位置;gzoffset 给出压缩文件偏移, 读取模式下会减去尚未使用的缓冲输入。两者不存在固定换算关系。

读取。 从逻辑位置 150,000,000 后退到 100,000,000,可能需要回到起点, 重新解码并丢弃前缀。部分工作会推迟到读取时执行,因此定位可能远慢于普通文件的跳转。

flowchart LR
    current["逻辑位置 150,000,000"] -->|"请求向后定位"| start["回到流起点"]
    start -->|"解码并丢弃前缀"| target["逻辑位置 100,000,000"]
    target -->|"下一次读取交付字节"| next["应用输出"]

向前定位可以消耗已解码缓冲,也可以安排稍后跳过;透明输入有直接文件定位路径。 证明须把已处理位置及待跳过量与可观察位置联系起来,并保证偏移计算可表示。 不支持 SEEK_END。

写入。 写入 ABC,定位到逻辑偏移 6,再写入 D:中间三个字节为零,按普通数据压缩。

七个未压缩字节单元格显示 ABC、向前定位插入的三个零字节,以及下标 6 处的 D。

颜色区分已有字节、零字节和新输入,不表示证明覆盖率。 写入时不能向后定位来修改 A。 补零可以推迟到 write/close,因此须跨调用保存待补距离,并处理后续 I/O 失败。 见定位、位置查询 和位置论证。 解码器检查点是另一种机制。

6.5 独立的校验和操作

adler32/crc32 可以在没有编解码器或文件句柄的情况下,随字节片段更新少量状态。 用 X、Y 表示两段按顺序拼接的字节,X || Y 表示先 X 后 Y。如果两段独立处理,可用两者校验和与 Y 的字节数,得到 X || Y 的校验和。 长度不可省略,合并校验和不是普通加法。

须在证明实现的界限与整数行为之外,证明这种组合关系。 见契约、Adler-32 和 CRC-32。包装层的连接见 第 4 章;验收证据统一记录于进度页。

ZLIB × LEAN

全局目录

当前位置6. 选择应用接口