小组研究成果被EMSOFT 2026接收

ACM SIGBED International Conference on Embedded Software（EMSOFT）是嵌入式软件领域的重要国际学术会议之一，长期关注嵌入式软件设计、分析、验证、优化及软硬件协同等方向的前沿研究。2026年，清华大学软件系统安全保障小组共有1项研究成果被EMSOFT 2026接收。

该成果是“SECO: Towards Code Compaction for Simulink via Verified Equivalence Extraction”。该工作面向资源受限嵌入式设备中Simulink生成代码规模较大的问题，提出了一套基于可验证等价片段提取的代码压缩框架SECO。SECO利用Simulink模型中的子系统边界、参数信息和数据流语义，引导大语言模型识别结构不同但语义等价的代码片段，并将其提取为可复用的共享函数；同时，通过约束检查、自动化验证函数生成、CBMC与SMT求解器等价性验证以及目标平台预编译分析，仅保留语义正确且能够实际减小代码规模的优化结果。实验在8个Simulink模型以及ARM、TriCore和RISC-V三类代表性嵌入式架构上开展。结果表明，在面向代码规模优化的-Oz配置下，SECO相较Simulink Embedded Coder、Frodo和SalSSA，平均减少55.6%的汇编代码规模，同时仅引入1.0%的平均运行时间开销。该工作由清华大学博士生喻泽弘、北京航空航天大学副教授苏卓、清华大学硕士生邱浩伟等人参与完成，北京航空航天大学副教授苏卓和清华大学教授姜宇等人共同指导。

该工作的核心洞察是：Simulink生成代码中的冗余并不总是表现为代码结构或语法形式完全相同。受子系统结构、参数取值、控制条件和表达式组织方式等因素影响，功能相关的模型组件可能生成表面差异明显、但能够由同一共享函数统一表达的代码片段。现有代码生成器和编译器主要依赖结构匹配或语法相似性，难以识别这类深层语义等价关系。针对这一点，SECO利用Simulink模型语义为大语言模型提供代码划分和分析上下文，引导其发现潜在的等价代码片段；同时引入形式化等价性验证，确保共享函数能够安全替换原始代码。SECO的主要流程包含三个核心阶段：Semantic-Aided Generation、LLM-Assisted Extraction和Semantic Equivalence Checking。

语义辅助生成（Semantic-Aided Generation）： 为了让大语言模型理解生成代码背后的Simulink模型语义，SECO首先使用Simulink Embedded Coder生成目标模型的嵌入式代码，并解析Simulink模型文件，提取子系统结构、模块属性及连接关系等信息。在此基础上，SECO通过子系统嵌入，在生成代码中标记各个子系统对应的代码边界；通过参数化将不同子系统中的常量替换为统一的参数变量，避免数值差异掩盖潜在的代码等价关系；同时根据模型连接关系构建数据流图，记录各操作之间的数据依赖以及相关变量的属性。经过语义增强后，原本缺少模型层次信息的生成代码能够保留子系统边界、参数关系和数据流语义，为后续等价代码识别提供更加明确的分析上下文。

大语言模型辅助等价提取（LLM-Assisted Extraction）： SECO使用等价提取智能体分析增强后的代码，从子系统级和代码片段级两个层次识别可以合并的候选片段，并为其生成统一的共享函数。为提高识别准确性，SECO在提示中提供典型的等价模式、非等价反例以及候选片段和共享函数的格式约束。考虑到大语言模型可能生成参数遗漏、变量类型错误或语法不合法的代码，SECO进一步设计约束检查智能体，对函数签名、输入输出参数、局部变量及候选片段格式进行检查，并调用编译器验证语法正确性。当编译失败时，智能体根据编译器反馈迭代修复代码，从而将大语言模型生成的初步结果转化为格式规范且能够正常编译的候选优化方案。

语义等价性验证（Semantic Equivalence Checking）： 由于能够编译并不意味着共享函数与原始代码在语义上等价，SECO不会直接采用大语言模型生成的优化结果。对于每个候选代码片段，SECO首先将其映射到对应的数据流子图，据此确定输入参数、输出参数和局部变量，并自动生成封装原始计算逻辑的验证函数。随后，SECO将验证函数与共享函数组合为验证程序，利用CBMC和SMT求解器检查两者在所有有效输入下是否产生一致输出。若验证失败，SECO提取导致差异的输入和输出反例，并将其反馈给等价提取智能体进行修正；经过多次尝试仍无法通过验证的候选片段将被保守丢弃。对于通过等价性验证的改写，SECO还会分别预编译原始代码和优化代码，仅保留能够在目标平台上实际减小代码规模的共享函数，最终同时保证代码改写的语义正确性和压缩收益。