FreeRTOS CBMC 形式化证明解析QueueCreateCountingSemaphoreStatic 的内存安全证明【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS本文围绕 QueueCreateCountingSemaphoreStatic 证明文档 展开讲解 FreeRTOS 官方 CBMCC Bounded Model Checker验证框架中针对QueueCreateCountingSemaphoreStatic这一内核 API 的内存安全证明它证明了什么、依赖哪些前置假设、harness 与构建配置如何编写以及如何在本地完整运行该证明并解读结果。读完本文你可以理解 FreeRTOS 形式化验证体系的组织方式并具备独立运行、扩展单条 CBMC 证明的能力。一、证明对象与前提假设xQueueCreateCountingSemaphoreStatic是 FreeRTOS 计数信号量的“静态分配”创建接口调用者自行提供队列结构体与控制块所在的存储区StaticQueue_t *由内核完成初始化。这类 API 的内存安全不越界读、不越界写、空指针解引用受控是内核正确性的基础也是 CBMC 证明的重点对象。证明文档明确给出了本条证明成立所依赖的核心前提uxMaxCount 0最大计数值必须为正uxInitialCount uxMaxCount初始计数不超过最大计数指向存储区的引用pxStaticQueue参数不为空。在上述假设成立的前提下harness 证明了QueueCreateCountingSemaphoreStatic的内存安全性。文档同时声明该证明仍处于work-in-progress进行中状态并明确它额外假设以下两个端口层函数是内存安全的、且不产生与本函数内存安全相关的副作用vPortEnterCriticalvPortExitCritical这一声明体现了 CBMC 证明的通用方法论每条叶子证明聚焦单一入口点把临界区进入/退出等硬件相关函数视为可信的内存安全前提从而避免证明爆炸proof explosion同时保证对当前被证函数内存安全结论的局部完备性。二、证明目录的文件组成该证明位于 proofs/Queue 目录 下与其相邻的还有QueueCreateCountingSemaphore、QueueCreateMutex、QueueCreateMutexStatic、QueueGenericCreate、QueueGenericCreateStatic等兄弟证明覆盖了队列/信号量/互斥量创建、收发、复位、互斥锁获取等全部队列族 API说明QueueCreateCountingSemaphoreStatic是队列创建族证明中的一员。本证明目录包含 4 个文件文件作用README.md证明目标与假设说明本文主体文档QueueCreateCountingSemaphoreStatic_harness.c证明 harness构造未定义输入并调用被证函数Makefile.json证明构建配置入口函数、CBMC 参数、参与对象、宏定义cbmc-viewer.jsoncbmc-viewer 报告生成配置三、Harness 源码逐行解读harness 是 CBMC 证明的“入口程序”负责把被证函数暴露给模型检查器。本证明的 harness 全文如下见 QueueCreateCountingSemaphoreStatic_harness.c#include FreeRTOS.h #include queue.h #include cbmc.h void harness() { UBaseType_t uxMaxCount; UBaseType_t uxInitialCount; StaticQueue_t * pxStaticQueue ( StaticQueue_t * ) pvPortMalloc( sizeof( StaticQueue_t ) ); xQueueCreateCountingSemaphoreStatic( uxMaxCount, uxInitialCount, pxStaticQueue ); }三个值得注意的技术细节未定义输入即非确定性输入。uxMaxCount与uxInitialCount是未初始化的局部变量CBMC 会将其解释为任意值——这正是“穷举所有输入组合”的手段证明对一切uxMaxCount、uxInitialCount取值下函数都不会发生越界访问违反 README 声明的假设组合则不在证明范围内。存储区由 harness 动态分配。pxStaticQueue通过pvPortMalloc( sizeof( StaticQueue_t ) )获得一块恰好容纳StaticQueue_t的内存这保证了 README 中“存储区引用非空”这一前提且分配尺寸与结构体精确匹配——若被证函数对该存储区的访问超出sizeof( StaticQueue_t )CBMC 会报告越界错误。返回值被丢弃。harness 不检查xQueueCreateCountingSemaphoreStatic的返回值说明本条证明只针对内存安全属性不覆盖返回值/功能性断言。四、Makefile.json 构建配置解析Makefile.json 采用 FreeRTOS CBMC 基础设施的统一 JSON 格式由prepare.py脚本在构建期展开为各平台 Makefile。关键字段如下{ ENTRY: QueueCreateCountingSemaphoreStatic, 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 ], GENERATE_HEADER: [ queue_datastructure.h ] }逐项说明ENTRY声明本证明的入口点为QueueCreateCountingSemaphoreStatic与 README 中“本 harness 证明 QueueCreateCountingSemaphoreStatic 的内存安全”一一对应OBJS中的$(ENTRY)_harness.goto即由该 harness 编译出的 goto 中间表示文件。CBMCFLAGS--unwind 1限制循环展开 1 次防止循环导致的展开爆炸--signed-overflow-check与--unsigned-overflow-check额外把整数溢出纳入检查——对信号量计数这类算术密集路径尤其重要能捕获计数增减过程中的溢出隐患。OBJS参与验证的翻译单元只有 harness、queue.c队列实现与list.cFreeRTOS 内核列表管理队列内部用List_t维护等待任务三个对象从构建依赖关系可以看出被证函数实现落在队列模块且其内存安全结论依赖list.c的相关操作。DEF将configUSE_TRACE_FACILITY与configGENERATE_RUN_TIME_STATS配置为 0裁剪掉运行时统计代码路径缩小验证状态空间。GENERATE_HEADER声明queue_datastructure.h为构建期生成的头文件供 harness 与内核源码共享内部数据结构定义。五、在本地运行该证明运行方法以 CBMC 基础设施总 README 为准该文档同时是所有叶子证明的统一入口。前提与步骤如下环境前提当前仅支持 Python 构建路径运行于 Linux 与 MacOSWindows 用户经 WSLPython ≥ 3.7、Make64 位机器上安装 32 位 gcc 库例如sudo apt-get install gcc-multilib安装 CBMC 工具链确保cbmc、goto-ccWindows 下为goto-cl、goto-instrument均可在命令行执行如需生成报告安装cbmc-viewer。操作步骤# 1. 确保内核子模块已拉取本仓库以 submodule 方式引入内核 git submodule update --init --recursive --checkout # 2. 在 proofs 目录展开各证明的 Makefile cd FreeRTOS/Test/CBMC/proofs python3 prepare.py # 3. 进入本证明目录并运行 cd Queue/QueueCreateCountingSemaphoreStatic make结果解读make会在证明目录下生成 HTML 与 JSON 两种报告对应目录内的cbmc-viewer.json配置HTML 报告可在浏览器中打开运行成功时报告的Errors区域显示None即表明在 harness 所述假设下xQueueCreateCountingSemaphoreStatic的内存安全属性成立。总 README 还说明CI 系统会对每个 pull request运行全部证明本地make即是与 CI 相同的验证动作。六、基础设施背景与证明边界从源码结构看本证明依赖的公共基础设施包括include/cbmc.hharness 中#include cbmc.h引用的断言辅助接口include/queue_init.h针对configUSE_QUEUE_SETS 1时prvCopyDataToQueue的 stub 与内存安全断言——该头文件注释明确解释prvCopyDataToQueue与prvNotifyQueueSetContainer联合使用会导致状态空间爆炸故拆分为独立证明这也解释了为何 proofs/Queue 目录 中prvCopyDataToQueue、prvNotifyQueueSetContainer各自拥有独立的证明目录patches 目录运行前对内核源码应用补丁去除static与volatile限定符使模型检查器能够正确跟踪跨翻译单元的指针别名。同时需要明确本证明的边界避免过度解读其结论它只证明内存安全不证明返回值语义、调度行为等属性它依赖前提假设uxMaxCount 0、uxInitialCount uxMaxCount、存储区非空不满足假设的输入不在覆盖范围它把vPortEnterCritical/vPortExitCritical视为可信函数临界区本身的正确性属于端口层实现的责任文档自述为 work-in-progress假设的完整清单以 harness 源码为准。作为对照同级的 QueueGenericCreateStatic 证明文档 采用了同样的假设声明范式其关键假设是(uxItemSize * uxQueueLength) sizeof(Queue_t)不溢出、存储区尺寸正确并额外覆盖configSUPPORT_DYNAMIC_ALLOCATION取 0 与 1 两种配置——可以看出队列族静态创建类证明在假设表述上保持了一致的风格QueueCreateCountingSemaphoreStatic的三条假设正是该风格在信号量场景下的具体化。小结FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic这条证明以约 10 行 harness 一份 JSON 构建配置给出了xQueueCreateCountingSemaphoreStatic在“uxMaxCount 0、uxInitialCount uxMaxCount、存储区非空、端口临界区函数内存安全”前提下的内存安全机器可检验证明。理解它即掌握了 FreeRTOS CBMC 验证框架“单入口点 harness 假设 prepare.py 生成 Makefile CI 全量回归”的完整工作模式可据此复现、阅读乃至为其他队列族 API 编写同构的新证明。【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考