FreeRTOS CBMC 验证补丁集详解：patches 目录的三大类补丁与自动化应用工具链

FreeRTOS CBMC 验证补丁集详解patches 目录的三大类补丁与自动化应用工具链【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOSFreeRTOS 仓库的FreeRTOS/Test/CBMC/目录构建了一套用 C Bounded Model CheckerCBMC对内核各 API 做内存安全自动验证的完整基础设施而 patches 目录 正是其中承上启下的一环它存放一组在运行证明前必须临时应用到内核源码上的补丁使 CBMC 能够分析那些原本无法直接验证的内部实现。本文以 patches/README.md 为核心逐类剖析目录中每一个补丁的改动内容与动因并结合 patch.py、unpatch.py、Makefile 与 compute_patch.py 等配套工具完整讲清补丁从哪来、如何应用、如何撤销、如何自动生成。读完本文你既能理解每处补丁为何不改变内核行为却能解锁验证能力也能在本地复现补丁的申请与回滚流程。1. 背景为什么运行 CBMC 证明需要一组补丁FreeRTOS/Test/CBMC/README.md 说明该目录包含对 FreeRTOS 代码库各部分内存安全性的自动证明持续集成系统会用这些证明校验每一个 Pull Request开发者也可以在本地运行。证明使用 CBMC 这一开源静态分析工具要求cbmc、goto-ccWindows 上为goto-cl与goto-instrument三个程序均可从命令行调用Python 版本需不低于 3.7另需 Make 构建工具在 64 位机器上还需安装 32 位 gcc 库如 Linux 上的gcc-multilib。CBMC 基础设施的目录划分为引自 CBMC/README.md 的Proof directory structure一节proofs每个 Pull Request 都会运行的证明每个叶子目录对应 FreeRTOS 单个入口点的内存安全证明patches运行证明前会应用到代码库上的一组补丁用于移除源码中的 static 和 volatile 限定符include与windows证明所用的头文件。当前仓库中 proofs 下按模块组织Task子目录包含 TaskCreate、TaskDelay、TaskDelete、TaskSuspendAll、TaskSwitchContext 等十余个证明目录Queue子目录包含 QueueGenericSend、QueuePeek、QueueReceive 等二十余个证明目录其中就有与补丁直接同名的三个目录prvCopyDataToQueue、prvNotifyQueueSetContainer、prvUnlockQueue见 proofs/Queue。后文会解释这三者之间的对应关系。2. 补丁的三大类别patches/README.md 将本目录的补丁归为三类The patches fall into three classes:First is a refactoring of prvCheckOptionsSecond is the removal of static attributes from some functionsThird is two patches dealing with shortcomings of CBMC that should be removed soon.对应地目录中实际存在的补丁文件按文件名编号为补丁文件目标文件类别0005-Remove-volatile-qualifier-from-tasks-variables.patchtasks.c第三类应对 CBMC 局限0005-remove-static-from-prvCopyDataToQueue.patchqueue.c第二类移除 static0006-Remove-static-from-prvNotifyQueueSetContainer.patchqueue.c第二类移除 static0007-Remove-static-from-prvUnlockQueue.patchqueue.c第二类移除 static0008-Fix-preemption-macro-for-queueYIELD_IF_USING_PREEMPT.patchqueue.c第三类应对 CBMC 局限除补丁文件外目录还包含头文件配置副本FreeRTOSConfig.h、FreeRTOSIPConfig.h、构建脚本Makefile与自动化工具patch.py、unpatch.py、compute_patch.py、patches_constants.py。下面逐类展开。3. 第一类prvCheckOptions 的重构README 提到的第一类补丁是对prvCheckOptions函数的重构。需要如实说明的是在当前仓库快照中针对prvCheckOptions的检索仅命中 patches/README.md 本身的这一句描述目录内并没有对应的.patch文件。从源码结构看这处重构要么已被合并进内核主线、其补丁文件随之移除要么属于 README 滞后于目录现状的说明——读者在对照其他分支或上游历史时应留意这一点。其余两类补丁则是当前目录的主体下面重点解析。4. 第二类补丁移除内部函数的 static 限定符三个补丁分别移除queue.c中三个内部函数的static存储限定且都同时改动前置声明与函数定义两处保证声明一致0005-remove-static-from-prvCopyDataToQueue.patch将static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void * pvItemToQueue, const BaseType_t xPosition )的前置声明与定义均去掉static0006-Remove-static-from-prvNotifyQueueSetContainer.patch对prvNotifyQueueSetContainer( const Queue_t * const pxQueue )做同样处理该函数位于#if ( configUSE_QUEUE_SETS 1 )条件编译块内0007-Remove-static-from-prvUnlockQueue.patch对prvUnlockQueue( Queue_t * const pxQueue )做同样处理。这三个函数是 FreeRTOS 队列子系统的核心内部路径prvCopyDataToQueue负责把数据项写入队列头部或尾部prvNotifyQueueSetContainer在队列有数据时通知其所属的 queue setprvUnlockQueue在调度器挂起状态下维护队列锁计数并在解锁时决定是否需要解除阻塞。移除static的直接动机可以从证明目录的组织方式得到印证proofs/Queue 下恰好存在与这三个函数同名的证明目录prvCopyDataToQueue/、prvNotifyQueueSetContainer/、prvUnlockQueue/。CBMC 证明为每个入口点建立一个独立的证明工程若要直接对某个函数建立证明前提与断言该函数需要在证明上下文中以外部链接形式可见static会把函数限定在单个编译单元内部成为外部证明入口访问该函数的障碍。这三处补丁只改动存储类声明不触碰任何函数体逻辑因此不改变内核行为只是打开验证通道。5. 第三类补丁应对 CBMC 局限的两处修改README 将第三类描述为处理 CBMC 局限、且希望尽快移除的补丁对应 volatile 限定符移除补丁与 0008 抢占宏补丁两个文件。5.1 移除 tasks.c 中三个全局变量的 volatile 限定符0005-Remove-volatile-qualifier-from-tasks-variables.patch 的 diff 改动如下节选-PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList; -PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList; PRIVILEGED_DATA static List_t * pxDelayedTaskList; PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList; ... -PRIVILEGED_DATA static volatile TickType_t xPendedTicks ( TickType_t ) 0U; PRIVILEGED_DATA static TickType_t xPendedTicks ( TickType_t ) 0U;该补丁文件自身带有极为详尽的注释解释了背后的验证学原因值得完整继承对任务池task pool证明goto-instrument以--nondet-volatile标志运行使每次读取 volatile 变量都变成非确定性读取可能返回任意值。对一般 volatile 变量来说这恰好是验证所需的语义但当 volatile 变量是指针时问题就出现了解引用一个 volatile 指针时可能取值之一是NULL导致证明中出现无法排除的空指针路径对xPendedTickstasks.c 中紧随其后的循环补丁注释引用了 tasks.c 第 2231–2255 行的代码块先做一份非 volatile 拷贝再迭代{ UBaseType_t uxPendedCounts uxPendedTicks; /* Non-volatile copy. */ if( uxPendedCounts ( UBaseType_t ) 0U ) { do { if( xTaskIncrementTick() ! pdFALSE ) { xYieldPending pdTRUE; } else { mtCOVERAGE_TEST_MARKER(); } --uxPendedCounts; } while( uxPendedCounts ( UBaseType_t ) 0U ); uxPendedTicks 0; } else { mtCOVERAGE_TEST_MARKER(); } }若uxPendedTicks的读取是非确定性的uxPendedCounts可能取任意值CBMC 无法对该do-while循环做展开unwind/unroll证明因此不可完成。所以必须让xPendedTicks表现得像普通变量。也就是说这个补丁在验证语义保真与可判定性之间做了取舍牺牲 volatile 的完全非确定性换取循环可展开、指针路径可收敛。补丁注释也明确了这是临时手段——一旦工具链对 volatile 的处理改进即可移除。5.2 修复 queueYIELD_IF_USING_PREEMPTION 宏的结构0008-Fix-preemption-macro-for-queueYIELD_IF_USING_PREEMPT.patch 修改 queue.c 中抢占式让出宏的#if嵌套结构节选#define queueYIELD_IF_USING_PREEMPTION() -#else - #if ( configNUMBER_OF_CORES 1 ) - #define queueYIELD_IF_USING_PREEMPTION() portYIELD_WITHIN_API() - #else /* #if ( configNUMBER_OF_CORES 1 ) */ - #define queueYIELD_IF_USING_PREEMPTION() vTaskYieldWithinAPI() - #endif /* #if ( configNUMBER_OF_CORES 1 ) */ #endif #if ( configNUMBER_OF_CORES 1 ) ( configUSE_PREEMPTION 1 ) #define queueYIELD_IF_USING_PREEMPTION() portYIELD_WITHIN_API() #endif #if ( configNUMBER_OF_CORES 1 ) ( configUSE_PREEMPTION 1 ) #define queueYIELD_IF_USING_PREEMPTION() vTaskYieldWithinAPI() #endif改动前后的语义是等价的协作式调度下宏展开为空单核 抢占式下展开为portYIELD_WITHIN_API()多核 抢占式下展开为vTaskYieldWithinAPI()。区别在于原写法用#if/#else链宏定义嵌套在configUSE_PREEMPTION判断的#else分支内部而改写后把核数 抢占模式的条件显式合并进各自的#if条件中消除了深层嵌套。这类改写属于典型的为静态分析器预处理器展开铺路的等价重构CBMC 在分析前需要完整展开条件编译扁平化的条件结构使其能够正确求出该宏在给定配置下的展开结果。6. 补丁的应用、回滚与幂等保护补丁如何进入内核源码工具链提供了两套等价路径。6.1 Python 路径patch.py 与 unpatch.pypatch.py 的核心逻辑幂等保护若 patches 目录中已存在patched标记文件直接退出避免重复打补丁逐个应用对目录内每个*.patch执行git apply --ignore-space-change --ignore-whitespace patch工作目录设为上溯四级的仓库根目录补丁的 diff 路径形如a/FreeRTOS/Source/queue.c相对仓库根解析结果记录无论成败都写入patched标记文件其中分Success:与Failure:两栏列出各补丁文件的相对路径便于后续排查某个补丁失败通常意味着内核版本与补丁基线不匹配。unpatch.py 与之对称先删除patched标记不存在时提示Nothing to do here.并退出再对每个*.patch执行git apply -R反向应用完成撤销失败时打印Unpatching failed: file。6.2 Makefile 路径生成、打补丁、还原三位一体patches/Makefile 定义了三个目标defaultgit format-patch freertos..freertos-cbmc-patches即从基线分支freertos到 CBMC 补丁分支freertos-cbmc-patches之间导出补丁序列——这解释了0005–0008这类顺序编号的来源patch若patched标记不存在则从patches上溯三级的目录逐个执行patch -p1 CBMC/patches/file随后创建空的patched标记unpatchgit checkout ../../../lib还原内核子库的工作区并删除标记文件。Makefile 末尾的注释patching file lib/FreeRTOS-Plus-TCP/...等还透露了该工具链曾服务于 FreeRTOS-Plus-TCP 源码的历史说明这套应用前快照、应用后打标记、还原时整目录 checkout的设计是跨内核与协议栈复用的通用模式。6.3 补丁基线与内核子模块补丁的 diff 路径FreeRTOS/Source/queue.c、FreeRTOS/Source/tasks.c表明其应用目标是仓库中的内核源码树CBMC/README.md 也要求先执行git submodule update --init --recursive --checkout拉齐所有子模块否则补丁的上下文行对不上git apply会失败并被记入patched文件的Failure:栏。这也给出了一个实用的自检点应用后检查patched文件任何一条 Failure 都说明当前内核基线与补丁不匹配需要先对齐版本。7. 配套机制compute_patch.py 自动生成头文件宏补丁patches 目录中还有一组用于宏配置注入的自动化工具与手动维护的.patch文件分工不同它不修改内核 C 源文件而是围绕证明使用的三个头文件生成auto_patch_*.patch。patches_constants.py 定义了两个关键常量PATCHES_DIR os.path.dirname(os.path.abspath(__file__)) HEADERS [os.path.join(absolute_prefix, FreeRTOSConfig.h), os.path.join(absolute_prefix, FreeRTOSIPConfig.h), os.path.join(absolute_prefix_port, portmacro.h)]其中portmacro.h指向Source/portable/MSVC-MingW移植层shared_prefix_port指定说明该证明工具链的默认验证目标是 Windows 移植层与 CBMC 顶层目录 下并列的windows子目录相呼应。compute_patch.py 的处理流程脚本自述generates patch files for the header files used in the cbmc proof. These patches permit setting values of preprocessor macros as part of the proof configuration收集宏名find_all_defines遍历 proofs 目录解析每个证明目录的Makefile.json取DEF键或MakefileCommon.json取DEF键用正则(\w)提取形如macro(x)false、configASSERT(X)__CPROVER_assert(x, must hold)的命令行宏定义中的宏名并容忍 JSON 中的注释行非标准 JSON需先剔除改写头文件manipulate_headerfile对三个头文件中被证明配置引用的每个#define若其上方没有#ifndef 同名宏保护就为其包裹一对#ifndef 宏 ... #endif支持以\结尾的多行定义。效果是证明构建通过命令行-D传入的宏值会覆盖头文件内置值而未被证明引用的宏保持原样落盘为补丁create_patch改写后执行git diff生成差异随即git checkout --还原头文件把差异写入auto_patch_头文件名.patch脏工作区保护header_dirty先跑git status与git diff-files确认工作区干净、目标头文件未被修改注释说明这是针对 MacOS 上git apply -R不刷新 diff-files 状态的变通否则抛出DirtyGitError中止自测脚本内置unittestTestDefineRegexes覆盖DEFINE_REGEX_MAKEFILE与DEFINE_REGEX_HEADER对带引号、带括号、带赋值等多种宏定义写法的匹配可通过python3 -m unittest compute_patch.py运行。被这套机制管理的 FreeRTOSConfig.h 是一份面向证明环境的完整内核配置例如其中configUSE_PREEMPTION 1、configMAX_PRIORITIES ( 7 )、configTICK_RATE_HZ ( 1000 )、configTOTAL_HEAP_SIZE ( 2048U * 1024U )、configUSE_MUTEXES 1等取值正是各证明目录Makefile.json中DEF宏覆盖的对象。8. 与证明流程的衔接从打补丁到出报告把上述机制放回整体流程按 CBMC/README.md 的Setting up the proofs在仓库根执行git submodule update --init --recursive --checkout拉齐子模块后进入 proofs 目录运行python3 prepare.py生成各证明目录的 MakefileWindows 宿主可传--system linux/--system windows交叉生成随后进入某个证明叶子目录如 proofs/Task/TaskCreate执行make。make产出 HTML 与 JSON 两份报告分别位于该目录的html/html与html/json下浏览器打开html/html/index.htmlErrors一栏显示None即表示该入口点的内存安全证明通过。本目录补丁在这一流程中的位置非常明确static 移除补丁让prvCopyDataToQueue、prvNotifyQueueSetContainer、prvUnlockQueue这三个内部函数成为可被独立证明引用的入口——与 proofs/Queue 下三个同名证明目录一一对应volatile 移除补丁保证 tasks.c 中挂起计数循环可被 CBMC 展开支撑 Task 侧如 proofs/Task 的 TaskIncrementTick、TaskSuspendAll 等证明的终止性0008 宏结构补丁确保抢占让出宏在证明配置下被预处理器正确展开compute_patch 生成的宏补丁则让每个证明能以命令行宏覆盖 FreeRTOSConfig.h 等头文件中的默认配置实现同一份内核源码、多套验证配置。9. 小结patches 目录 的 README 虽然只有寥寥数行却准确概括了整套补丁的设计哲学所有修改都严格遵循不改内核行为、只解除验证障碍的原则——去掉static是打开函数可见性去掉volatile与扁平化抢占宏是为goto-instrument/CBMC 的可判定性让路而 patch.py/unpatch.py 的标记文件幂等机制、Makefile 的分支间 format-patch 导出、以及 compute_patch.py 的宏注入流水线共同保证了这些临时改动可重复应用、可完全回滚、且不污染内核主线。对于希望深入 FreeRTOS 形式化验证的读者建议从 proofs/Queue/prvCopyDataToQueue 这类补丁与证明同名的最小案例入手对照补丁文件与证明目录逐行阅读即可完整复现一条内存安全证明的闭环。【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考