📚 课程目录第3章 Polyspace工具链与工作流概览

3. Polyspace工具链与工作流概览

在把 Stateflow 模型纳入静态分析质量体系之前，必须先厘清 Polyspace 工具链中各个组件分别解决什么问题、它们之间如何协作，以及分析结果从哪里来、到哪里去。很多团队在初次引入 Polyspace 时，容易把 Bug Finder 和 Code Prover 当成"两个版本的同一种工具"，或者把 Client/Server 配置理解为单纯的许可证问题，结果导致分析目标错位、报告无法解释。本节从工具职责、部署形态、与 Simulink/Stateflow 的集成方式三个维度展开，并给出从模型到分析报告的端到端流程。

一、Bug Finder 与 Code Prover：两类互补的分析引擎

Polyspace 的核心分析能力由两个引擎承担，它们的定位有本质区别。

Polyspace Bug Finder 面向"缺陷检测"，采用静态分析加抽象解释的混合策略，在有限时间内扫描代码，找出运行时错误、并发问题、安全编码违规、代码质量缺陷等。它的输出是"发现的问题清单"，每个问题带有严重等级（如 High/Medium/Low）、缺陷类型（如数组越界、空指针解引用、数据竞争）、代码位置和调用路径。Bug Finder 不追求证明，而是追求在可接受时间内尽可能多地暴露可疑点，因此结果中可能包含需要人工确认的告警。

Polyspace Code Prover 面向"形式化验证"，对每个变量、每个运算、每个分支做抽象域上的穷尽分析，最终给出三类结论：绿色表示该处不可能发生运行时错误（已证明安全）、红色表示确定存在错误路径、橙色表示无法证明也无法证伪（可能存在问题，需要人工审查或补充约束）。Code Prover 的价值在于"证明"而非"发现"，它能回答"这段代码是否绝对不会有除零"这类问题，代价是分析时间更长、对代码规模和复杂度更敏感。

两者不是替代关系，而是配合关系：Bug Finder 用于日常快速扫描和缺陷收敛，Code Prover 用于关键模块的深度验证和适航、功能安全认证证据。实际项目中常见的做法是先用 Bug Finder 做全量扫描，把红色问题清零，再对安全相关模块用 Code Prover 做证明级分析。

二、Client/Server 配置：分析任务的部署形态

Polyspace 支持两种运行形态。单机（Client）模式下，用户在本地机器上通过 Polyspace 桌面端或命令行启动分析，所有计算在本机完成，适合小规模代码和调试阶段。Client/Server 模式下，客户端只负责提交分析任务和查看结果，真正的分析计算在服务器端执行，适合大型项目、多人协作和需要统一许可证管理的场景。

Client/Server 配置的关键在于三件事：一是服务器端需要安装 Polyspace Server 组件并配置好许可证服务；二是客户端通过 polyspace-server 相关配置指向服务器地址和端口；三是分析任务以作业（job）形式提交，结果回传到客户端或集中存储。这种形态下，分析可以排队、可以并行、可以跨平台，也便于把静态分析纳入 CI 流水线。

一个典型的命令行提交示例如下（示例参数，实际需按项目调整）：

polyspace-bug-finder -sources src/controller.c \
  -include include/ \
  -results-dir ./results/bf_run1 \
  -server-host 10.20.30.40 -server-port 12427 \
  -checkers all -target x86_64

提交后，服务器执行分析，客户端通过结果目录或 Web 界面查看。需要注意的是，服务器端和客户端的 Polyspace 版本应保持一致，否则结果格式可能不兼容。

三、与 Simulink/Stateflow 的集成方式

Stateflow 模型本身不是 C 代码，Polyspace 不能直接分析 .slx 文件。集成的核心思路是：先把 Stateflow 生成的代码提取出来，再对代码做静态分析。Simulink 提供了两种主要路径。

第一种是代码生成后分析。通过 Embedded Coder 将包含 Stateflow 的模型生成 C/C++ 代码，再用 Polyspace 对生成代码进行分析。这种方式最贴近最终产品代码，能发现生成代码中的实际缺陷，但需要配置好代码生成选项（如目标处理器、编译器抽象层），并注意生成代码中的 rtwtypes.h、model.h 等依赖文件要一并纳入分析范围。

第二种是模型级集成分析。Polyspace 提供与 Simulink 的集成接口，可以在 Simulink 环境中直接对模型或子系统启动分析，工具会自动调用代码生成并衔接分析流程。这种方式适合在建模阶段就快速获得反馈，但分析深度和可配置性通常不如直接对生成代码分析。

无论哪种路径，都需要关注 Stateflow 特有的分析对象：状态机的状态转移条件、转移动作、默认转移、并行状态、历史节点等。这些结构在生成代码中会体现为 switch 语句、状态变量和转移函数，Polyspace 的分析结果需要结合 Stateflow 语义来解读，不能只看代码行号。

四、从模型到分析报告的端到端流程

把上述组件串起来，一个完整的端到端流程包含以下环节：模型准备（确认 Stateflow 图表可生成代码、配置代码生成目标）→ 代码生成（Embedded Coder 输出 C/C++ 及依赖文件）→ 分析配置（选择 Bug Finder 或 Code Prover、指定检查项、设置目标平台和编译选项）→ 提交分析（本地或 Client/Server）→ 结果审查（按严重等级和缺陷类型分类，逐条确认或标记）→ 报告导出（生成 HTML/PDF 报告，纳入质量记录）→ 问题修复与回归（修改模型或代码后重新分析，确认问题关闭）。

这个流程中，最容易被忽视的是"结果审查"环节。Polyspace 的输出不是"通过/不通过"的二元结论，而是带有置信度的告警集合。审查时需要区分：确定缺陷（必须修复）、误报（需要调整分析配置或添加约束）、可接受风险（需要记录理由）。只有完成这一步，分析报告才具备质量证据的价值。