cbmc/codedetect/examples/freertos

FreeRTOS验证示例

本目录包含使用CodeDetect系统验证FreeRTOS代码的完整示例。这些示例展示了如何在实时操作系统环境中进行形式化验证，包括任务管理、队列操作、同步机制和中断处理。

示例概览

1. 任务验证示例 (task_verification_example.c)

文件: task_verification_example.c

功能: 演示FreeRTOS任务的创建、管理和验证

验证要点:

• 任务参数验证（NULL指针检查）
• 任务生命周期管理
• 栈空间使用验证
• 任务同步机制
• 内存安全性验证
• 任务状态一致性

关键代码片段:

void vCounterTask(void *pvParameters) {
    TaskParameters_t *params = (TaskParameters_t *)pvParameters;

    /* 参数验证 - CodeDetect将生成相应的CBMC规范 */
    configASSERT(params != NULL);
    configASSERT(params->task_id > 0);
    configASSERT(params->max_count > 0);

    /* 任务循环 */
    while (params->should_stop == pdFALSE) {
        /* 边界检查 - 防止计数器溢出 */
        if (params->counter < params->max_count) {
            params->counter++;
        }
        vTaskDelay(pdMS_TO_TICKS(100));
    }
}

2. 队列验证示例 (queue_verification_example.c)

文件: queue_verification_example.c

功能: 演示FreeRTOS队列操作的验证

验证要点:

• 队列创建和删除的安全性
• 队列满和空状态的处理
• 生产者-消费者模式验证
• 并发访问安全性
• 消息完整性检查
• 队列溢出保护

关键代码片段:

void vProducerTask(void *pvParameters) {
    if (xMessage.is_critical) {
        /* 关键消息使用更长等待时间 */
        xSendResult = xQueueSend(xMessageQueue, &xMessage, pdMS_TO_TICKS(100));
    } else {
        /* 普通消息使用较短等待时间 */
        xSendResult = xQueueSend(xMessageQueue, &xMessage, pdMS_TO_TICKS(10));
    }

    /* 错误处理 */
    if (xSendResult != pdPASS) {
        xQueueStats.queue_full_errors++;
    }
}

验证模式

1. 基本验证

目标: 验证代码的基本正确性

• 内存安全
• 空指针处理
• 边界条件
• 资源管理

CBMC规范生成:

void test_task_safety() {
    TaskParameters_t params;
    vCounterTask(&params);
    __CPROVER_assert(params.counter >= 0, "counter_non_negative");
}

2. 并发验证

目标: 验证多任务环境下的安全性

• 竞态条件检测
• 死锁预防
• 数据一致性
• 同步机制验证

CBMC规范生成:

void test_concurrent_access() {
    QueueHandle_t queue = xQueueCreate(10, sizeof(int));
    /* CodeDetect生成并发访问验证规范 */
    __CPROVER_assert(queue != NULL, "queue_creation_success");
}

3. 性能验证

目标: 验证实时性能要求

• 响应时间保证
• 内存使用限制
• 执行时间分析
• 资源使用效率

CodeDetect集成

1. 配置文件

创建 freertos_config.yaml:

freertos:
  include_headers:
    - "FreeRTOS.h"
    - "task.h"
    - "queue.h"
    - "semphr.h"
  config_path: "/path/to/FreeRTOSConfig.h"
  heap_size: 4096
  max_tasks: 10
  stack_size: 1024

verification:
  target_types: ["memory_safety", "concurrency", "overflow_detection"]
  timeout: 300
  max_concurrent_jobs: 4

2. 验证流程

1. 代码解析: 分析FreeRTOS代码结构
2. 规范生成: 基于LLM生成CBMC验证规范
3. 规范突变: 生成变异规范提高覆盖率
4. CBMC验证: 运行形式化验证
5. 结果分析: 生成详细验证报告

3. API使用示例

from src.verify.cbmc_runner import CBMCRunner
from src.mutate.engine import MutationEngine

# 创建验证器
runner = CBMCRunner()
engine = MutationEngine()

# 解析FreeRTOS代码
metadata = parse_freertos_code("task_example.c")

# 生成验证规范
specifications = generate_freertos_specs(metadata)

# 生成突变规范
mutations = engine.generate_mutations(
    specifications[0],
    metadata,
    max_mutations=10
)

# 运行验证
results = []
for mutation in mutations:
    result = await runner.run_verification(
        function_metadata=metadata[0],
        source_file="task_example.c",
        specification=mutation.specification
    )
    results.append(result)

验证报告

典型验证结果

=== FreeRTOS任务验证报告 ===

文件: task_verification_example.c
函数: vCounterTask
验证时间: 2.34s

✅ 内存安全: 通过
  - 无空指针解引用
  - 无缓冲区溢出
  - 无内存泄漏

✅ 并发安全: 通过
  - 任务同步正确
  - 无数据竞争
  - 栈空间充足

✅ 边界检查: 通过
  - 计数器溢出保护
  - 参数范围验证
  - 循环终止条件

⚠️  性能警告:
  - 任务延时时间较长 (100ms)
  - 栈使用率较高 (85%)

建议:
1. 考虑减少任务延时以提高响应性
2. 增加栈大小或优化内存使用

高级验证场景

1. 中断处理验证

void vISR_Handler(void) {
    BaseType_t xHigherPriorityTaskWoken = pdFALSE;

    /* 中断安全的关键区域 */
    taskENTER_CRITICAL_FROM_ISR();

    /* 处理中断 */
    xQueueSendFromISR(xQueue, &data, &xHigherPriorityTaskWoken);

    taskEXIT_CRITICAL_FROM_ISR();

    /* 必要时进行任务切换 */
    portYIELD_FROM_ISR(xHigherPriorityTaskWoken);
}

验证要点:

• 中断上下文安全性
• 关键区域保护
• 任务切换时机
• 数据一致性保证

2. 内存管理验证

void* pvAllocateManagedMemory(size_t xSize) {
    void* pvReturn = pvPortMalloc(xSize);

    if (pvReturn != NULL) {
        /* 追踪内存分配 */
        vTrackAllocation(pvReturn, xSize);
    }

    return pvReturn;
}

验证要点:

• 内存分配失败处理
• 内存泄漏检测
• 堆空间溢出保护
• 内存对齐要求

3. 信号量和互斥量验证

void vProtectedFunction(void) {
    /* 获取互斥量 */
    if (xSemaphoreTake(xMutex, portMAX_DELAY) == pdTRUE) {
        /* 受保护的代码区域 */
        vCriticalOperation();

        /* 释放互斥量 */
        xSemaphoreGive(xMutex);
    }
}

验证要点:

• 死锁预防
• 优先级反转
• 资源泄漏
• 超时处理

最佳实践

1. 代码编写

• 参数验证: 始终验证函数参数
• 错误处理: 正确处理FreeRTOS API返回值
• 资源管理: 确保分配的资源被正确释放
• 并发安全: 使用适当的同步机制

2. 验证策略

• 增量验证: 先验证基本功能，再验证复杂场景
• 边界测试: 重点测试边界条件和错误情况
• 性能分析: 监控内存使用和执行时间
• 覆盖率最大化: 使用突变测试提高验证覆盖率

3. 配置优化

# 生产环境验证配置
verification:
  depth: 25          # 增加搜索深度
  unwind: 15         # 增加循环展开
  timeout: 600       # 增加超时时间
  max_memory: "2GB"  # 增加内存限制

freertos:
  max_tasks: 20      # 支持更多任务
  stack_size: 2048   # 更大的栈空间
  heap_size: 8192    # 更大的堆空间

故障排除

常见问题

1. CBMC超时

   解决方案:
   - 减少验证深度 (--depth 15)
   - 增加超时时间 (--timeout 600)
   - 限制循环展开 (--unwind 5)
   

2. 内存不足

   解决方案:
   - 增加可用内存
   - 简化验证条件
   - 分批验证功能
   

3. 验证失败

   解决方案:
   - 检查反例路径
   - 验证前置条件
   - 增强错误处理
   - 修改算法逻辑
   

调试技巧

1. 逐步验证: 先验证简单函数，再验证复杂逻辑
2. 日志分析: 启用详细日志输出分析问题
3. 反例分析: 仔细分析CBMC生成的反例
4. 参数调优: 根据代码复杂度调整验证参数

扩展示例

1. 复杂任务间通信

创建 complex_communication_example.c 演示：

• 多个生产者和消费者
• 优先级调度
• 事件通知机制
• 复杂数据结构传递

2. 定时器和定时服务

创建 timer_verification_example.c 演示：

• 软件定时器验证
• 硬件定时器集成
• 定时器回调安全性
• 时间精度保证

3. 外设驱动验证

创建 driver_verification_example.c 演示：

• 硬件抽象层验证
• DMA操作安全性
• 中断驱动处理
• 外设配置验证

贡献指南

我们欢迎社区贡献新的FreeRTOS验证示例：

1. 创建示例: 在本目录添加新的.c文件
2. 添加文档: 包含详细的说明和验证要点
3. 测试验证: 确保示例可以通过验证
4. 提交PR: 通过GitHub提交Pull Request

许可证

本示例代码遵循与主项目相同的许可证条款。

---

最后更新: 2024年1月