FreeRTOS CBMC 内存安全证明QueueGetMutexHolderFromISR 校验案例全解析【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS本文以 FreeRTOS 仓库中FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR证明目录为切入点围绕官方文档对该证明的简短描述展开完整还原其校验 harness 的源码写法、Makefile.json中的 CBMC 参数配置以及该证明在整套 CBMC 证明基础设施中的运行方式与适用边界。读完后你将理解如何用 CBMCC Bounded Model Checker针对 FreeRTOS 队列 API 建立内存安全证明并能在本机按仓库文档流程复现该证明的执行与报告查看。证明定位与目录结构该证明位于 CBMC 证明目录树中按 API 入口点组织的叶级目录 FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR。根据上层 CBMC 证明基础设施说明proofs目录下的每个叶目录都对应FreeRTOS 中某个单一入口点的内存安全证明且这些证明会被持续集成系统用于校验仓库的每一个 Pull Request开发者也可以在本地机器上运行它们。该目录包含 4 个文件文件作用README.md证明说明文档本案例的核心关联文档QueueGetMutexHolderFromISR_harness.c校验 harness描述证明假设Makefile.jsonCBMC 证明的构建/参数配置cbmc-viewer.jsoncbmc-viewer 生成 HTML/JSON 报告所用的配置官方文档的核心声明关联文档 README.md 全文仅 5 行其核心信息为假设xSemaphore是指向一个已分配的Queue_t实例的指针本 harness 证明了QueueGetMutexHolderFromISR的内存安全性memory safety。该证明目前是一个进行中的工作work-in-progress证明假设proof assumptions描述在 harness 中。这三句话界定了本证明的三件事证明对象、前置假设、完成状态。下面结合目录中的实际文件把这三点逐一展开为可验证的源码级细节。校验 harness证明假设的源码载体harness 文件 QueueGetMutexHolderFromISR_harness.c版权头标注为 FreeRTOS V202212.00的关键内容如下#include FreeRTOS.h #include queue.h #include queue_datastructure.h #include cbmc.h void harness() { QueueHandle_t xSemaphore pvPortMalloc( sizeof( Queue_t ) ); if( xSemaphore ) { xQueueGetMutexHolderFromISR( xSemaphore ); } }结合文档声明假设xSemaphore是指向一个已分配的Queue_t实例的指针可以看到该假设是如何在代码中落实的分配而非取地址pvPortMalloc( sizeof( Queue_t ) )在堆上分配出与Queue_t等大的内存块而不是使用一个栈上的Queue_t变量或悬空指针。这保证了对xSemaphore的所有内存访问都落在合法分配的内存范围内——这正是指针指向已分配实例的机器可验证形式。NULL 检查if( xSemaphore )使证明域排除分配失败路径harness 只验证成功分配后的调用路径与已分配实例的假设保持一致。假设只描述在 harness 中文档明确证明假设描述在 harness 中即证明的入口、前置条件与后置期望全部收敛在这 40 行以内的文件中而不是散落在别处。另外两点从源码结构可以看出包含私有头queue_datastructure.hharness 直接引用了内核队列的内部数据结构头文件以便证明上下文能看到Queue_t的完整定义。与Makefile.json中GENERATE_HEADER项对应该头文件在构建准备阶段被生成详见下节。仅分配、不初始化harness 从未调用xQueueCreate/xSemaphoreCreateMutex等初始化 APIQueue_t各字段对 CBMC 而言是未定义值。从源码结构看这意味着该证明只约束不越界、不空指针解引用、不溢出这类内存安全性质而不验证返回值是否为正确的互斥持有者这类功能语义。被测函数xQueueGetMutexHolderFromISR本身属于 FreeRTOS 内核队列模块queue.c。在本仓库中内核源码是子模块FreeRTOS/Source.gitmodules指向 FreeRTOS-Kernel 仓库需要git submodule update --init --recursive --checkout拉取后才能看到queue.c的实现harness 与 Makefile 中的$(FREERTOS)/Source/queue.goto即指该子模块中的源文件。Makefile.jsonCBMC 证明参数逐项解析Makefile.json 是该证明的构建与求解配置去掉版权注释后的有效内容如下{ ENTRY: QueueGetMutexHolderFromISR, CBMCFLAGS: [ --unwind 1, --signed-overflow-check, --unsigned-overflow-check ], OBJS: [ $(ENTRY)_harness.goto, $(FREERTOS)/Source/queue.goto, $(FREERTOS)/Source/list.goto ], DEF: [ configUSE_TRACE_FACILITY0, configGENERATE_RUN_TIME_STATS0 ], INC: [ . ], GENERATE_HEADER: [ queue_datastructure.h ] }各配置项对证明行为的影响ENTRY声明被证明的入口点名称。$(ENTRY)占位符同时被用于定位 harness 文件QueueGetMutexHolderFromISR_harness.c这也是 harness 必须以ENTRY_harness.c命名的原因。CBMCFLAGS--unwind 1将循环展开上界设为 1即证明以每个循环至多展开一轮为界进行有界验证bounded model checking既控制求解规模也决定了证明的完整性边界--signed-overflow-check与--unsigned-overflow-check使 CBMC 把有符号/无符号整数溢出作为检查性质纳入证明因此该证明覆盖的范围不止指针越界还包括溢出类缺陷。OBJS列出参与证明的对象文件。除 harness 外还显式包含$(FREERTOS)/Source/queue.goto队列模块即被测函数所在文件与$(FREERTOS)/Source/list.goto链表模块队列内部依赖List_t数据结构被证明覆盖。.goto后缀表示这些.c文件由goto-cc编译为 GOTO 中间表示后再交给 CBMC 求解。DEF编译期宏定义。configUSE_TRACE_FACILITY0与configGENERATE_RUN_TIME_STATS0关闭了跟踪设施与运行时统计两个可选特性使被验证的代码路径收敛到最小内核配置与默认证明场景保持一致。GENERATE_HEADER声明queue_datastructure.h为生成头文件即构建准备脚本依据配置生成该头供 harness 与证明过程包含——这解释了为什么 harness 能直接#include queue_datastructure.h。INC将证明目录自身加入头文件搜索路径使#include cbmc.h等按目录内相对关系解析。在本机运行该证明按照 CBMC 证明基础设施 README 的说明整套证明目前仅支持基于 Python 的构建可在 Linux 与 macOS 上运行Windows 用户可借助 WSL。完整流程如下准备依赖Python ≥ 3.7、make64 位机器需安装 32 位 gcc 库如sudo apt-get install gcc-multilib。安装工具链安装 CBMC 后需保证命令行可执行cbmc、goto-ccWindows 下为goto-cl与goto-instrument安装 cbmc-viewer 后可执行cbmc-viewer用于生成报告。拉取子模块在 FreeRTOS 仓库根目录执行git submodule update --init --recursive --checkout确保内核源码FreeRTOS/Source等子模块就位。生成 Makefile进入proofs目录执行python3 prepare.py该脚本会在每个证明目录包括本案例的 QueueGetMutexHolderFromISR 目录中依据Makefile.json生成 Makefile。若需跨系统生成如在 Windows 上生成 Linux Makefile可传--system linux或--system windows选项。执行证明进入证明目录执行make证明可能耗时较长。查看结果make会生成 HTML 与 JSON 报告以基础设施 README 中 TaskCreate 的说明为参照报告输出在证明目录下的html/html与html/json子目录浏览器打开html/html/index.html后成功运行时Errors一节应显示None。本案例目录下随附的 cbmc-viewer.json 即报告生成的配置。需要说明的适用前提proofs/patches目录在证明运行前会对代码库打补丁用于移除源码中的static与volatile限定符include与windows目录提供证明所需的头文件——这些是运行证明前由准备脚本自动处理的环境细节本地复现时无需手工干预。证明的保证范围与work-in-progress边界回到关联文档的第三句话该证明目前是进行中的工作。结合 harness 与配置可以精确划定其当前保证边界保证在xSemaphore指向已分配的Queue_t实例这一前置假设下xQueueGetMutexHolderFromISR的调用路径中不存在内存安全违例空指针解引用、越界读写等且不发生有符号/无符号整数溢出。不保证harness 未初始化Queue_t字段故证明不覆盖返回值语义正确性等功能性质--unwind 1表明循环路径仅按单轮展开的有界条件验证对非互斥队列句柄传入该 ISR 接口时的行为语义同样不属于本证明的断言范围。从源码结构看work-in-progress的表述与--unwind 1的有界设置相吻合证明当前聚焦于最核心的内存安全性质完整性约束与功能假设的补强属于后续迭代方向。这也提示使用者在引用此类证明结论时应把假设在哪里描述本例即 harness 源码与边界如何设置Makefile.json中的 CBMCFLAGS作为第一手判读依据。小结本案例展示了 FreeRTOS 仓库中单一 API 入口 轻量 harness 声明式 Makefile.json的 CBMC 证明范式README.md 用 5 行文档锁定证明对象与假设harness 源码 将已分配Queue_t实例的假设落实为pvPortMalloc NULL 检查的可验证构造Makefile.json 以--unwind 1与溢出检查界定验证边界并显式纳入queue.c、list.c两个内核对象。遵循 CBMC 基础设施文档 的prepare.pymake两步流程即可在本机复现该证明并查看 HTML/JSON 报告。【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考